"Enter" key on Num block does not work anymore to submit tactic

leanprover-community / lean4game

Server to host lean games.

https://adam.math.hhu.de

GNU General Public License v3.0

198 stars 35 forks source link

"Enter" key on Num block does not work anymore to submit tactic #212

Closed Madjosz closed 7 months ago

Madjosz commented 7 months ago

Hitting the "Enter" key on the Num block does not submit the current tactic anymore. "Return" still works.

Tested in Firefox 124.0.2 (64-Bit) and Vivaldi 6.6.3271.61 (64-Bit).

joneugster commented 7 months ago

I think this should solve it. According to key codes I added NumpadEnter.

Will be live next time I update the server. You can probably test it at https://adam-dev.math.hhu.de from tomorrow on. Maybe you can confirm tomorrow if it works for you on the Test-server.

(I don't think I can test this myself easily, don't have a numpad)