New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix gen files #21

Merged

lemastero merged 3 commits into master from fix-gen-files

Dec 19, 2023

Owner

lemastero commented Dec 19, 2023

Changes

fix broken generating output files
improve CI to detect generating rs files

lemastero added 3 commits

December 18, 2023 23:46


          fix broken file generation

c2e79bb


          delete example file on CI

9cc794a


          update hello.agda

d112ac7

lemastero merged commit 6c45d5b into master

1 check passed

lemastero deleted the fix-gen-files branch

December 19, 2023 01:06

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet