Why:
The conditional needed is already present in idris-switch-working-directory and this fixes issue of unable to load files into Idris2 in different directories.
Steps to reproduce:
Given directory "a" with file foo.idr and directory "b" with bar.idr Then open a/foo.idr and load the file to Idris2 (M-x idris-load-file) Then open b/bar.idr and try load it to Idris2.
Current result:
Evaluation returned an error: Error loading file bar.idr: File Not Found. Expected:
bar.idr loaded to Idris2 and working directory switched to "b".
This change also aligns idris-load-file and idris-load-file-sync where the conditional was not included in past.
Also includes improvements to idris-switch-working-directory
Why: The conditional needed is already present in
idris-switch-working-directoryand this fixes issue of unable to load files into Idris2 in different directories.Steps to reproduce: Given directory "a" with file foo.idr and directory "b" with bar.idr Then open a/foo.idr and load the file to Idris2 (M-x idris-load-file) Then open b/bar.idr and try load it to Idris2.
Current result:
Evaluation returned an error: Error loading file bar.idr: File Not Found.Expected: bar.idr loaded to Idris2 and working directory switched to "b".This change also aligns
idris-load-fileandidris-load-file-syncwhere the conditional was not included in past.Also includes improvements to
idris-switch-working-directory