Robo can't find definitions of tactics or theorems

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪

https://adam.math.hhu.de

Apache License 2.0

16 stars 9 forks source link

Closed tautastic closed 1 month ago

tautastic commented 1 month ago

The current version of Robo can not display any definitions of tactics or theorems:

XHRGET
https://adam.math.hhu.de/data/g/hhu-adam/robo/doc__Tactic__tauto.json
[HTTP/1.1 404 Not Found 34ms]

The development version running on https://adam-dev.math.hhu.de uses doc__tauto.json instead of doc__Tactic__tauto.json.

This has probably to do with #56.

tautastic commented 1 month ago

Also fixed with #56