Work on adding user feedback by opening a github issue from game #251
+884
−495
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
See #218
This is work in progress.
So far, I have an extra dropdown option, which opens a popup with a button, which opens a GitHub issue with title and body prefilled. This 'UX workflow' probably needs to change a little bit, for example adding more context to the button, i.e. that this will create a GitHub issue)/
For now, I got as far as without playing a game to get the specific data of the level and the proof.
I am not sure in which directory I should place the local game I use for testing purposes. I placed the NNG4 repo dir in the directory of the lean4game
So output from
ls
looks something like this:This 'works', but I actually could not play the game locally, as it could not find the game.
![lean4game-github-issue](https://private-user-images.githubusercontent.com/16431833/349641464-49cba343-fb18-4266-b257-f00a67927cd9.png?jwt=eyJhbGciOiJIUzI1NiIsInR5cCI6IkpXVCJ9.eyJpc3MiOiJnaXRodWIuY29tIiwiYXVkIjoicmF3LmdpdGh1YnVzZXJjb250ZW50LmNvbSIsImtleSI6ImtleTUiLCJleHAiOjE3Mzk3NDUwMjYsIm5iZiI6MTczOTc0NDcyNiwicGF0aCI6Ii8xNjQzMTgzMy8zNDk2NDE0NjQtNDljYmEzNDMtZmIxOC00MjY2LWIyNTctZjAwYTY3OTI3Y2Q5LnBuZz9YLUFtei1BbGdvcml0aG09QVdTNC1ITUFDLVNIQTI1NiZYLUFtei1DcmVkZW50aWFsPUFLSUFWQ09EWUxTQTUzUFFLNFpBJTJGMjAyNTAyMTYlMkZ1cy1lYXN0LTElMkZzMyUyRmF3czRfcmVxdWVzdCZYLUFtei1EYXRlPTIwMjUwMjE2VDIyMjUyNlomWC1BbXotRXhwaXJlcz0zMDAmWC1BbXotU2lnbmF0dXJlPWZiM2U4NzI5NDc0ODEwMWQ0YTMxODBkZjI5ZjQzMGRmMjdmMWE4NzE0ZjRmNDliNjYzOTI4YzBiOGVmZTg3YzEmWC1BbXotU2lnbmVkSGVhZGVycz1ob3N0In0.t3q7s0v7eXHgRdSWvDMJ9S-JvxCeWcz8Ga2cVoj8_VE)
Also; for pushing changes, I need to remove the NNG4 directory.
In .gitignore, there is a pattern for
games/
, so maybe the game should be added under this directory, but I am not sure how (I tried different options related to http://localhost:3000/#/g/local/FOLDER, but they did not work for me).