git.iko.soy/Idris-dev
on master help sign in
Disable :! in IDE mode
commit83cf2f66c08ba948d7682cf51d931cd068eaae70 authorRyan Scott <ryan.gl.scott@gmail.com> dateTue 24 Jan 2017, 15:05 (10 years ago) parentb76d961
1 file changed+2−1
compare with master
unifiedsplit
src/Idris/REPL.hs+2−1
src/Idris/REPL.hs+2−1
@@ -590,7 +590,8 @@ splitName s = case reverse $ splitOn "." s of
590590idemodeProcess :: FilePath -> Command -> Idris ()
591591idemodeProcess fn Warranty = process fn Warranty
592592idemodeProcess fn Help = process fn Help
593−idemodeProcess fn (RunShellCommand cmd) = process fn (RunShellCommand cmd)
593+idemodeProcess fn (RunShellCommand cmd) =
594+ iPrintError ":! is not currently supported in IDE mode."
594595idemodeProcess fn (ChangeDirectory f) =
595596 do process fn (ChangeDirectory f)
596597 dir <- runIO $ getCurrentDirectory