Various fixes in manpages

 * hyphen meant as the ascii character should be escaped
 * lines starting with a dot have a special meaning


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11322 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 19 deletions

diff --git a/man/coqdoc.1 b/man/coqdoc.1
index c443e8b04..45fcafd24 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -54,7 +54,7 @@ Redirect the output into the file
 Output files into directory 
 .I dir 
 instead of current directory (option
--d does not change the filename specified with option -o, if any).
+\-d does not change the filename specified with option \-o, if any).
 .TP
 .B \-s, \ \-\-short
 Do not insert titles for the files. The default behavior is to insert
@@ -68,7 +68,7 @@ Suppress the header and trailer of the final document. Thus, you can
 insert the resulting document into a larger one.
 .TP
 .BI \-p \ string, \ \-\-preamble \ string
-Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with -html).
+Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html).
 .TP
 .BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file
 Considers the file `file' respectively as a .v (or .g) file or a .tex file.
@@ -114,7 +114,7 @@ it builds a table of contents into toc.html.
 .TP
 .B \-\-glob\-from \ file
 Make references using Coq globalizations from file file. (Such
-globalizations are obtained with Coq option -dump-glob).
+globalizations are obtained with Coq option \-dump\-glob).
 
 .TP
 .B \-\-no\-externals
@@ -129,22 +129,22 @@ Set base URL for the Coq standard library (default is http://coq.inria.fr/librar
 Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
 
 .TP
-.BI -R \ dir \  coqdir
+.BI \-R \ dir \  coqdir
 Map physical directory dir to Coq logical directory coqdir (similarly
-to Coq option -R).
+to Coq option \-R).
 .B Note: 
-option -R only has effect on the files following it on the command
+option \-R only has effect on the files following it on the command
 line, so you will probably need to put this option first.
 
 .SS Contents options
 
 .TP
-.B -g, \ --gallina
+.B \-g, \ \-\-gallina
 Do not print proofs.
 
 .TP
-.B -l, \ --light
-Light mode. Suppress proofs (as with -g) and the following commands:
+.B \-l, \ \-\-light
+Light mode. Suppress proofs (as with \-g) and the following commands:
 
         * [Recursive] Tactic Definition
         * Hint / Hints
@@ -153,29 +153,29 @@ Light mode. Suppress proofs (as with -g) and the following commands:
         * Implicit Argument / Implicits
         * Section / Variable / Hypothesis / End 
 
-The behavior of options -g and -l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
+The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above).
 
 .SS Language options
  
 Default behavior is to assume ASCII 7 bits input files.
 
 .TP 
-.B -latin1, \ --latin1
-Select ISO-8859-1 input files. It is equivalent to --inputenc latin1
---charset iso-8859-1.
+.B \-latin1, \ \-\-latin1
+Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1
+\-\-charset iso\-8859\-1.
 
 .TP 
-.B -utf8, \ --utf8
-Select UTF-8 (Unicode) input files. It is equivalent to --inputenc
-utf8 --charset utf-8. LATEX UTF-8 support can be found at
-http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
+.B \-utf8, \ \-\-utf8
+Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc
+utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at
+http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/.
 
 .TP 
-.BI --inputenc \ string
+.BI \-\-inputenc \ string
 Give a LATEX input encoding, as an option to LATEX package inputenc.
 
 .TP
-.BI --charset \ string
+.BI \-\-charset \ string
 Specify the HTML character set, to be inserted in the HTML header.