X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fcmdline.ml;h=ff71c9c98bd84b8089f3fe1cd49b58946b5e6f20;hb=9607fb2d34d679e14040f9132625a53f1de5200a;hp=f83d5eb77d70a38d14dc2c29ad2b44c72f617519;hpb=349ba0ff3bded60e8035d5896a6d5f689a632ae7;p=goals.git

diff --git a/src/cmdline.ml b/src/cmdline.ml
index f83d5eb..ff71c9c 100644
--- a/src/cmdline.ml
+++ b/src/cmdline.ml
@@ -52,6 +52,7 @@ let input_file = ref "Goalfile"
 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 () =
@@ -82,6 +83,12 @@ let parse () =
                    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,
@@ -128,4 +135,5 @@ let input_file () = !input_file
 let includes () = !includes
 
 let nr_jobs () = !nr_jobs
+let silent () = !silent
 let use_prelude () = !use_prelude