diff options
| author | notin | 2008-02-13 14:23:23 +0000 |
|---|---|---|
| committer | notin | 2008-02-13 14:23:23 +0000 |
| commit | 8c7d9c49e34ec0ba22f0e4c34c46b1bf36788308 (patch) | |
| tree | 9a6c16bbfb8c50254ebdad687240ede743cfb511 /tools | |
| parent | 5b5e0694d6e55b07c38e9d654206aef2b0964ea5 (diff) | |
Suppression de l'option -glob-from de Coqdoc: les globalisations sont
lues directement des fichiers .glob
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/main.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 7c97055a67..c3a32f08ff 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -51,7 +51,6 @@ let usage () = prerr_endline " --files-from <file> read file names to process in <file>"; prerr_endline " --quiet quiet mode (default)"; prerr_endline " --verbose verbose mode"; - prerr_endline " --glob-from <file> read Coq globalizations from file <file>"; prerr_endline " --no-externals no links to Coq standard library"; prerr_endline " --coqlib <url> set URL for Coq standard library"; prerr_endline " (default is http://coq.inria.fr/library/)"; @@ -64,6 +63,9 @@ let usage () = prerr_endline ""; exit 1 +let obsolete s = + eprintf "Warning: option %s is now obsolete; please update your scripts\n" s + (*s \textbf{Banner.} Always printed. Notice that it is printed on error output, so that when the output of [coqdoc] is redirected this header is not (unless both standard and error outputs are redirected, of @@ -311,7 +313,7 @@ let parse () = | "-R" :: ([] | [_]) -> usage () | ("-glob-from" | "--glob-from") :: f :: rem -> - Index.read_glob f; parse_rec rem + obsolete "glob-from"; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> usage () | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> @@ -372,7 +374,7 @@ let copy src dst = (*s Functions for generating output files *) - + let gen_one_file l = let file = function | Vernac_file (f,m) -> @@ -420,8 +422,13 @@ let gen_mult_files l = (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) +let glob_filename f = + (Filename.chop_extension f) ^ ".glob" + let index_module = function - | Vernac_file (_,m) -> Index.add_module m + | Vernac_file (f,m) -> + Index.read_glob (glob_filename f); + Index.add_module m | Latex_file _ -> () let produce_document l = |