diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-07 14:20:15 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-03-07 14:20:15 +0000 |
| commit | 266743d4345866520104ef20c807a22d7cea5e96 (patch) | |
| tree | 6b67391f6c4908a828e51a7b37cc95e4006dc85e /toplevel | |
| parent | c4d7fede86d052f1ffc824eb9a4aa7e3fdb63ea0 (diff) | |
raccourci -l en plus de -load-vernac-source
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2519 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
2 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c174877df..c70bab141 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -151,8 +151,9 @@ let parse_args () = | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem | "-load-ml-source" :: [] -> usage () - | "-load-vernac-source" :: f :: rem -> add_load_vernacular f; parse rem - | "-load-vernac-source" :: [] -> usage () + | ("-load-vernac-source"|"-l") :: f :: rem -> + add_load_vernacular f; parse rem + | ("-load-vernac-source"|"-l") :: [] -> usage () | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem | "-load-vernac-object" :: [] -> usage () diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 277cc7ad9..962fdcf78 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -33,6 +33,7 @@ let print_usage_channel co command = -load-ml-object f load ML object file f -load-ml-source f load ML file f -load-vernac-source f load Coq file f.v (Load f.) + -l f (idem) -load-vernac-object f load Coq object file f.vo -require f load Coq object file f.vo and import it (Require f.) -compile f compile Coq file f.v (implies -batch) |