Commit Graph
22 Commits
Author SHA1 Message Date
Jon Eugster b37f050da5 Merge pull request #204 from noamraph/patch-1
Update level.css - hide .katex-mathml, to fix scrolling issue
2024-03-25 18:51:48 +01:00
Noam Yorav-Raphael 09c81ea43f Update level.css - hide .katex-mathml, to fix scrolling issue
Fixes https://github.com/leanprover-community/lean4game/issues/202
2024-03-25 19:10:33 +02:00
Jon Eugster a9447a70d4 add interface buttons for i18n #179 2024-03-23 01:11:42 +01:00
Jon Eugster 47297e4194 temporary fix to improve message on server crash 2024-03-11 17:33:06 +01:00
Jon Eugster 1796c76a84 remove debugging css 2024-02-29 01:27:26 +01:00
Jon Eugster 3775ad98c8 level completed message in editor 2024-02-14 18:36:19 +01:00
Jon Eugster 6472ef5b31 First big junk of communication refactor 2024-02-07 12:50:39 +01:00
ran ab98eaa3ba Change the selected button to a slider 2024-01-16 11:21:46 +08:00
ran 8c93b3c5b3 Modify logic for all preferences 2024-01-12 23:29:03 +08:00
Jon Eugster 5a78118bb6 improve display of buttons on mobile 2023-12-14 23:04:18 +01:00
Jon Eugster eaa214ec37 improve world tree on mobile #101 2023-12-14 21:59:47 +01:00
Jon Eugster aec196deff add button to copy inventory item name to clipboard #144 2023-12-14 20:26:31 +01:00
Jon Eugster 93c55dc9f7 Merge pull request #167 from Wzixiao/home-button-margin
Adjust the margin of the home button.
2023-12-12 13:43:21 +01:00
Jon Eugster aab7441323 Merge pull request #166 from Wzixiao/app-bar-align-center
Adjust the top navigation bar to center both the Home button and some divs on the right.
2023-12-12 13:42:00 +01:00
ran 2ba36b91d5 Adjust the margin of the home button 2023-12-12 19:51:20 +08:00
ran a2726ae287 Adjust the top navigation bar so that it is centered above and below 2023-12-12 19:29:21 +08:00
Jon Eugster a1a6862b5a add tmp option to test images 2023-12-08 10:18:00 +01:00
Jon Eugster 54bab2a016 add support for images 2023-12-08 00:39:45 +01:00
joneugster 1b3993ad3e fix 2023-11-17 22:45:02 +01:00
Alexander Bentkamp 7e0b82cb14 better handling of breaking connection 2023-10-31 15:34:54 +01:00
joneugster d52d63020c fix dropdown on safari 2023-10-27 14:00:54 +02:00
joneugster e740027144 move css files 2023-10-23 18:07:55 +02:00