search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
197 stars 35 forks source link

Feature request: Allow options for deleting information #199

Open djvelleman opened 8 months ago

djvelleman commented 8 months ago

Currently, if you want to delete game information, your only option is to delete everything. Perhaps there could be a way to select the levels or worlds from which you want to delete information. One option would be to delete all information.

joneugster commented 8 months ago

I think an option to select/deselect individual worlds for deletion would be reasonable!