remove reference to column number parameter

idris-lang · Sep 27, 2024 · adc3f96 · adc3f96
1 parent 0e83d6c
commit adc3f96
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 7 deletions.
diff --git a/bootstrap/idris2_app/idris2.rkt b/bootstrap/idris2_app/idris2.rkt