diff options
| author | Tim King <taking@google.com> | 2015-10-29 17:42:52 -0700 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-10-29 17:42:52 -0700 |
| commit | b035877b01e8b8c2ea902d9f3732cf84bfed0fdf (patch) | |
| tree | f307ffbb1b2f8fd4d5edac2684538f294288b102 /src/theory/quantifiers | |
| parent | b455f5cde8b84b7951d309604b75a76afd8b8bfa (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.
Diffstat (limited to 'src/theory/quantifiers')
0 files changed, 0 insertions, 0 deletions