projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b455f5c) | patch
Removes an extra dollar sign from src/options/mktagheaders. The extra dollar sign...
authorTim King <taking@google.com>
Fri, 30 Oct 2015 00:42:52 +0000 (17:42 -0700)
committerTim King <taking@google.com>
Fri, 30 Oct 2015 00:42:52 +0000 (17:42 -0700)
commitb035877b01e8b8c2ea902d9f3732cf84bfed0fdf
treef307ffbb1b2f8fd4d5edac2684538f294288b102tree
parentb455f5cde8b84b7951d309604b75a76afd8b8bfacommit | diff
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.
src/options/mktagheaders diff | blob | history