Proper escaping in option documentation.

diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in
index baae1dc4bc60e71472c372f1da90531abe72e597..e08a96b1150543a693d3848a76f2fa2d4a220d02 100644 (file)
--- a/doc/cvc4.1_template.in
+++ b/doc/cvc4.1_template.in
@@ -46,13 +46,13 @@ is connected to a terminal, interactive mode is assumed.
 
 .SH COMMON OPTIONS
 
-.IP "Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the option."
+.IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option."
 
 ${common_manpage_documentation}
 
 ${remaining_manpage_documentation}
 
-.IP "Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the option."
+.IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option."
 
 .\".SH FILES
 .\".SH ENVIRONMENT

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 32f81455b65750fa3de239eb169199839a6a59df..de0986de1494a18e1fb9b44000f7f167a28033ca 100755 (executable)
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -1124,6 +1124,11 @@ $@"
       mandoc="$mandoc [*]"
     fi
 
+    # in man, minus sign is \-, different from hyphen
+    the_manopt="`echo "$the_opt" | sed 's,-,\\\\\\-,g'`"
+    mandoc="`echo "$mandoc" | sed 's,-,\\\\\\-,g'`"
+    mansmtdoc="`echo "$mansmtdoc" | sed 's,-,\\\\\\-,g'`"
+
     if [ "$the_opt" ]; then
       doc_line=
       while [ -n "$the_doc" ]; do
@@ -1147,14 +1152,14 @@ $@"
 #line $lineno \"$kf\"
 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
         common_manpage_documentation="${common_manpage_documentation}
-.IP \"$the_opt\"
+.IP \"$the_manopt\"
 $mandoc"
       elif [ "$category" != UNDOCUMENTED ]; then
         remaining_documentation="${remaining_documentation}\\n\"
 #line $lineno \"$kf\"
 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
         remaining_manpage_documentation="${remaining_manpage_documentation}
-.IP \"$the_opt\"
+.IP \"$the_manopt\"
 $mandoc"
       fi
     fi
@@ -1286,19 +1291,22 @@ function doc-alternate {
       the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
     done
 
+    # in man, minus sign is \-, different from hyphen
+    the_manopt="`echo "$the_opt" | sed 's,-,\\\\\\-,g'`"
+
     if [ "$category" = COMMON ]; then
       common_documentation="${common_documentation}\\n\"
 #line $lineno \"$kf\"
 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
       common_manpage_documentation="${common_manpage_documentation}
-.IP \"$the_opt\"
+.IP \"$the_manopt\"
 $@"
     else
       remaining_documentation="${remaining_documentation}\\n\"
 #line $lineno \"$kf\"
 \"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
       remaining_manpage_documentation="${remaining_manpage_documentation}
-.IP \"$the_opt\"
+.IP \"$the_manopt\"
 $@"
     fi
   else