From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 19 Jun 2014 02:02:15 +0000 (-0400)
Subject: Proper escaping in option documentation.
X-Git-Tag: cvc5-1.0.0~6758^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=73a0b6758acccf1d9ef7393be4e7f78dccabd17f;p=cvc5.git

Proper escaping in option documentation.
---

diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in
index baae1dc4b..e08a96b11 100644
--- 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 32f81455b..de0986de1 100755
--- 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