diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-27 18:00:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-27 18:00:59 +0000 |
| commit | 2b1e771f49be6794bbe7e7d2f54b7571ccdf35b3 (patch) | |
| tree | 3a8f963f7046bc5846a07aee3994d91db9847d28 /tools/coqdoc/main.ml | |
| parent | 05f7d5c2564bb10fa09853b088aac1b063496c6e (diff) | |
Added option --external to coqdoc to bind an url to an external library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/main.ml')
| -rw-r--r-- | tools/coqdoc/main.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index d2b66f993..7fb9322d7 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -56,6 +56,7 @@ let usage () = prerr_endline " --quiet quiet mode (default)"; prerr_endline " --verbose verbose mode"; prerr_endline " --no-externals no links to Coq standard library"; + prerr_endline " --external <url> <d> set URL for external library d"; prerr_endline " --coqlib <url> set URL for Coq standard library"; prerr_endline (" (default is " ^ Coq_config.wwwstdlib ^ ")"); prerr_endline " --boot run in boot mode"; @@ -349,6 +350,8 @@ let parse () = usage () | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> Cdglobals.externals := false; parse_rec rem + | ("--external" | "-external") :: u :: logicalpath :: rem -> + Index.add_external_library logicalpath u; parse_rec rem | ("--coqlib" | "-coqlib") :: u :: rem -> Cdglobals.coqlib := u; parse_rec rem | ("--coqlib" | "-coqlib") :: [] -> @@ -568,6 +571,7 @@ let produce_output fl = let main () = let files = parse () in + Index.init_coqlib_library (); if not !quiet then banner (); if files <> [] then produce_output files |