mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
Editor was made run apostrophe-containing modules from REPL normally.
This commit is contained in:
parent
9990b5ad29
commit
60c8695a6d
@ -706,7 +706,7 @@ process Edit
|
||||
Nothing => pure NoFileLoaded
|
||||
Just f =>
|
||||
do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts)
|
||||
coreLift $ system (editor opts ++ " " ++ f ++ line)
|
||||
coreLift $ system (editor opts ++ " \"" ++ f ++ "\"" ++ line)
|
||||
loadMainFile f
|
||||
process (Compile ctm outfile)
|
||||
= compileExp ctm outfile
|
||||
|
@ -2,3 +2,6 @@
|
||||
Module'> 2
|
||||
Module'> Bye for now!
|
||||
"5"
|
||||
Module'> Loaded file Module'.idr
|
||||
Module'>
|
||||
Bye for now!
|
||||
|
1
tests/idris2/basic048/input-ed
Normal file
1
tests/idris2/basic048/input-ed
Normal file
@ -0,0 +1 @@
|
||||
:e
|
@ -1,4 +1,5 @@
|
||||
$1 --no-banner --no-color --console-width 0 "Module'.idr" < input
|
||||
$1 --exec main --cg ${IDRIS2_TESTS_CG} "Module'.idr"
|
||||
EDITOR=true $1 --no-banner --no-color --console-width 0 "Module'.idr" < input-ed
|
||||
|
||||
rm -rf build
|
||||
|
Loading…
Reference in New Issue
Block a user