Closed gallais closed 2 years ago
Idris2 does not have .ibc files so this code is useless (and actively harmful if you try to load a .tex file that happens to be a literate idris file).
Good catch!
Idris2 does not have .ibc files so this code is useless (and actively harmful if you try to load a .tex file that happens to be a literate idris file).