From: Tim King <taking@google.com>
Date: Fri, 30 Oct 2015 00:42:52 +0000 (-0700)
Subject: Removes an extra dollar sign from src/options/mktagheaders. The extra dollar sign... 
X-Git-Tag: cvc5-1.0.0~6181
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b035877b01e8b8c2ea902d9f3732cf84bfed0fdf;p=cvc5.git

Removes an extra dollar sign from src/options/mktagheaders. The extra dollar sign came in as a copy paste from a Makefile. This was not proper bash.
---

diff --git a/src/options/mktagheaders b/src/options/mktagheaders
index 63a19bc23..5ef3b3172 100755
--- a/src/options/mktagheaders
+++ b/src/options/mktagheaders
@@ -14,7 +14,7 @@ TAG_FILE=$1
 
 echo 'static char const* const '$TAG_FILE'[] = {';
 for tag in `cat $TAG_FILE`; do
-  echo "\"$$tag\",";
+  echo "\"$tag\",";
 done;
 echo 'NULL';
 echo '};'