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

Merged

jespercockx merged 1 commit intoagda:masterfrom jespercockx:Issue201

Oct 11, 2023

+8-1

Commits on Oct 11, 2023

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