Jon Eugster
|
45d84103c1
|
bump npm packages
|
12 months ago |
|
Jon Eugster
|
92e9ed38b2
|
add manual trigger to github action
|
12 months ago |
|
Jon Eugster
|
2b85386373
|
move Hint tactic back
|
1 year ago |
|
Jon Eugster
|
8008b68fd6
|
cleanup code surrounding hints
|
1 year ago |
|
Jon Eugster
|
2649f985fa
|
plug-in variables in hints client-side
|
1 year ago |
|
Jon Eugster
|
3775ad98c8
|
level completed message in editor
|
1 year ago |
|
Jon Eugster
|
780514e45a
|
fix: allow theorems from inventory #191
|
1 year ago |
|
Jon Eugster
|
19f2ceface
|
fix indent
|
1 year ago |
|
Jon Eugster
|
800d1f3308
|
drop importGraph dependency in server
|
1 year ago |
|
Jon Eugster
|
c0acde14e2
|
hints and diags in editor
|
1 year ago |
|
Jon Eugster
|
976d1c6901
|
fix: goal in editor didnt show
|
1 year ago |
|
Jon Eugster
|
5bb6c559bc
|
update npm deps
|
1 year ago |
|
Jon Eugster
|
11ee6c1535
|
bump npm dependencies
|
1 year ago |
|
Jon Eugster
|
3998fb2fc9
|
Merge branch 'main' into dev
|
1 year ago |
|
Jon Eugster
|
538f74004c
|
allow for empty lines in editor
|
1 year ago |
|
Jon Eugster
|
6aebb8993f
|
update proof from editor
|
1 year ago |
|
Jon Eugster
|
6472ef5b31
|
First big junk of communication refactor
|
1 year ago |
|
Jon Eugster
|
72ffab5b46
|
cleanup InteractiveGoal
|
1 year ago |
|
Jon Eugster
|
3b660c5185
|
Merge branch 'dev'. Bump to v4.5.0
|
1 year ago |
|
Jon Eugster
|
ebb8c98145
|
bump to v4.5.0
|
1 year ago |
|
Jon Eugster
|
4abf05b77e
|
Merge branch 'dev' into v4.5.0-bump
|
1 year ago |
|
Jon Eugster
|
df423aaace
|
Merge pull request #181 from Wzixiao/auto-mobile-layout
Modify logic for preferences
|
1 year ago |
|
Jon Eugster
|
a67dcb306f
|
fix indent
|
1 year ago |
|
Jon Eugster
|
37582e04d4
|
fix errors for disabled tactics #188
|
1 year ago |
ran
|
9d4a6df139
|
Remove MobileContext and use PreferencesContext instead
|
1 year ago |
|
Jon Eugster
|
26202e5f36
|
fix typo
|
1 year ago |
|
Jon Eugster
|
ed017fa605
|
documentation & cleanup in FileWorker
|
1 year ago |
|
Jon Eugster
|
36bc52c960
|
add logic game to landing page
|
1 year ago |
|
Jon Eugster
|
e085f2f106
|
Merge pull request #186 from Geoc2022/main
Cleaned up Documentation
|
1 year ago |
|
Jon Eugster
|
e975c455fe
|
Update doc/DOCUMENTATION.md
|
1 year ago |
geo
|
c006be5a9f
|
Fix minor typos
|
1 year ago |
|
geo
|
49379a0930
|
Fix link references
|
1 year ago |
|
geo
|
03076b0161
|
Add example `npm start` message
|
1 year ago |
|
geo
|
bfb60ffedd
|
Updated "Doc entries"
|
1 year ago |
|
Jon Eugster
|
ca576542ba
|
whitelist generalizing and says. #173
|
1 year ago |
|
Jon Eugster
|
fd5e507541
|
lint: fix line widths
|
1 year ago |
|
Jon Eugster
|
c103eeacfa
|
fix: case insensitive url in local store #183
|
1 year ago |
|
Jon Eugster
|
e277a48749
|
add changelog file
|
1 year ago |
|
Jon Eugster
|
16ff701518
|
Update troubleshoot.md
|
1 year ago |
|
Jon Eugster
|
20ca385e14
|
Update README.md
|
1 year ago |
|
Jon Eugster
|
5a38543e3b
|
Merge pull request #185 from leanprover-community/joneugster-patch-1
Update docs
|
1 year ago |
|
Jon Eugster
|
a4a6f2e725
|
Merge pull request #184 from leanprover-community/joneugster-patch-1-1
Create troubleshoot.md
|
1 year ago |
|
Jon Eugster
|
cc89e78e4c
|
Create troubleshoot.md
|
1 year ago |
|
Jon Eugster
|
c533a635c2
|
Update docs
|
1 year ago |
|
ran
|
ab98eaa3ba
|
Change the selected button to a slider
|
1 year ago |
|
Jon Eugster
|
7114a8c4cb
|
fix: remove tmp files after import
|
1 year ago |
|
Jon Eugster
|
b7eb15184d
|
Merge pull request #182 from lnay/patch-1
Minor: correct error in markdown
|
1 year ago |
Luke Naylor
|
892c70165a
|
Minor: correct error in markdown
|
1 year ago |
|
ran
|
8929813e48
|
Added a missing space regarding code style in store.ts
|
1 year ago |
|
ran
|
5d88cd6739
|
Remove logically duplicated code
|
1 year ago |