git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Implement keep-going (-k) option.
[goals.git]
/
src
/
cmdline.ml
diff --git
a/src/cmdline.ml
b/src/cmdline.ml
index
927dfdf
..
86e9dbf
100644
(file)
--- a/
src/cmdline.ml
+++ b/
src/cmdline.ml
@@
-53,6
+53,7
@@
let input_file = ref "Goalfile"
let includes = ref [stdlibdir]
let add_include dir = includes := dir :: !includes
let nr_jobs = ref (nprocs ())
let includes = ref [stdlibdir]
let add_include dir = includes := dir :: !includes
let nr_jobs = ref (nprocs ())
+let keep_going = ref false
let silent = ref false
let use_prelude = ref true
let silent = ref false
let use_prelude = ref true
@@
-84,6
+85,10
@@
let parse () =
jobshelp;
"--no-prelude",Arg.Clear use_prelude,
" Do not automatically use prelude.gl from stdlib";
jobshelp;
"--no-prelude",Arg.Clear use_prelude,
" Do not automatically use prelude.gl from stdlib";
+ "-k", Arg.Set keep_going,
+ " Keep going after an error";
+ "--keep-going",Arg.Set keep_going,
+ " Keep going after an error";
"-s", Arg.Set silent,
" Silent operation";
"--silent", Arg.Set silent,
"-s", Arg.Set silent,
" Silent operation";
"--silent", Arg.Set silent,
@@
-136,5
+141,6
@@
let input_file () = !input_file
let includes () = !includes
let nr_jobs () = !nr_jobs
let includes () = !includes
let nr_jobs () = !nr_jobs
+let keep_going () = !keep_going
let silent () = !silent
let use_prelude () = !use_prelude
let silent () = !silent
let use_prelude () = !use_prelude