Open jfdm opened 3 months ago
Commit https://github.com/idris-hackers/idris-mode/commit/334fef6932a979fd3c59b26814c52682afc93406 introduced a loading error if given project which contains a source directory.
The error was along the lines of:
Error: Source file "Main.idr" is not in the source directory
We should introduce a test to capture this.
Commit https://github.com/idris-hackers/idris-mode/commit/334fef6932a979fd3c59b26814c52682afc93406 introduced a loading error if given project which contains a source directory.
The error was along the lines of:
We should introduce a test to capture this.