git.annexia.org
/
goals.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
maintainer: Add maintainer-commit, maintainer-tag goals.
[goals.git]
/
src
/
cmdline.ml
diff --git
a/src/cmdline.ml
b/src/cmdline.ml
index
f83d5eb
..
927dfdf
100644
(file)
--- a/
src/cmdline.ml
+++ b/
src/cmdline.ml
@@
-41,7
+41,8
@@
let print_version () =
(* Get stdlib directory. *)
let datadir =
(* Get stdlib directory. *)
let datadir =
- try Sys.getenv "GOALS_DATADIR" with Not_found -> Config.datadir
+ try Sys.getenv "GOALS_DATADIR"
+ with Not_found -> Config.datadir // "goals"
let stdlibdir = datadir // "stdlib"
let prelude_gl_file = stdlibdir // "prelude.gl"
let prelude_sh_file = stdlibdir // "prelude.sh"
let stdlibdir = datadir // "stdlib"
let prelude_gl_file = stdlibdir // "prelude.gl"
let prelude_sh_file = stdlibdir // "prelude.sh"
@@
-52,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 silent = ref false
let use_prelude = ref true
let parse () =
let use_prelude = ref true
let parse () =
@@
-82,6
+84,12
@@
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";
+ "-s", Arg.Set silent,
+ " Silent operation";
+ "--silent", Arg.Set silent,
+ " Silent operation";
+ "--quiet", Arg.Set silent,
+ " Silent operation";
"-v", Arg.Unit print_version,
" Print version and exit";
"--version", Arg.Unit print_version,
"-v", Arg.Unit print_version,
" Print version and exit";
"--version", Arg.Unit print_version,
@@
-128,4
+136,5
@@
let input_file () = !input_file
let includes () = !includes
let nr_jobs () = !nr_jobs
let includes () = !includes
let nr_jobs () = !nr_jobs
+let silent () = !silent
let use_prelude () = !use_prelude
let use_prelude () = !use_prelude