Jon Eugster
|
e07570181c
|
typo
|
2 years ago |
|
Jon Eugster
|
87689e1c3a
|
dont show 'intermediate goal solved' on error
|
2 years ago |
|
Jon Eugster
|
47297e4194
|
temporary fix to improve message on server crash
|
2 years ago |
|
Jon Eugster
|
8008b68fd6
|
cleanup code surrounding hints
|
2 years ago |
|
Jon Eugster
|
2649f985fa
|
plug-in variables in hints client-side
|
2 years ago |
|
Jon Eugster
|
538f74004c
|
allow for empty lines in editor
|
2 years ago |
|
Jon Eugster
|
6472ef5b31
|
First big junk of communication refactor
|
2 years ago |
|
Jon Eugster
|
614b762b6c
|
rename LemmaDoc into TheoremDoc and so on
|
3 years ago |
Alexander Bentkamp
|
97dc648452
|
use goal lctx for hints
Closes #135
|
3 years ago |
|
joneugster
|
44f7b6703e
|
Revert "fix variables in hints"
This reverts commit 8851cd8b1f.
|
3 years ago |
|
joneugster
|
8851cd8b1f
|
fix variables in hints
|
3 years ago |
|
Alexander Bentkamp
|
6580afb622
|
fix names in hints
Fixes #135
|
3 years ago |
|
Alexander Bentkamp
|
eaf0d13c2f
|
make game directory more configurable
|
3 years ago |
|
Jon Eugster
|
8246ae6eac
|
change folder structure
|
3 years ago |