From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 21 Jun 2014 22:11:39 +0000 (-0400)
Subject: Minor fixes for man pages.
X-Git-Tag: cvc5-1.0.0~6754
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75ec455661ecc88a8b9f77f7b913c227b7f3e728;p=cvc5.git

Minor fixes for man pages.
---

diff --git a/src/options/mkoptions b/src/options/mkoptions
index f05de0571..681eba808 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -1061,6 +1061,8 @@ function doc {
               mansmtdoc="$mansmtdoc (EXPERTS only)"
             fi
             altmanopt="`echo "$altopt" | sed 's,-,\\\\\\-,g'`"
+            mansmtdoc="`echo "$mansmtdoc" | sed 's,-,\\\\\\-,g'`"
+            typedefault="`echo "$typedefault" | sed 's,-,\\\\\\-,g'`"
             if [ "$category" = COMMON ]; then
               common_manpage_internals_documentation="${common_manpage_internals_documentation}
 .TP
@@ -1184,6 +1186,7 @@ $mandoc"
       else
         typedefault="($type, default = $default_value)"
       fi
+      typedefault="`echo "$typedefault" | sed 's,-,\\\\\\-,g'`"
       if [ "$category" = COMMON ]; then
         common_manpage_internals_documentation="${common_manpage_internals_documentation}
 .TP