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 #201 ] Drop backend when running in interactive mode #204

Merged

jespercockx merged 1 commit into agda:master from jespercockx:Issue201

Oct 11, 2023

Member

jespercockx commented Oct 11, 2023

Fixes #201


          [ fix agda#201 ] Drop backend when running in interactive mode

f156493

jespercockx merged commit 46c5473 into agda:master

6 checks passed

jespercockx added this to the 1.1 milestone

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

Labels

None yet