diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-04-19 15:42:39 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-19 15:42:39 -0700 |
| commit | 9b062e5b7e8478d78dabaf60701d647b7aaa9b6e (patch) | |
| tree | 07746351f8083fbe0fdcab5e6c2dcfb2a0877fe9 | |
| parent | 70046d35f2aff41867cbb6490e5bf6d026dc55a1 (diff) | |
Adding config/tap-driver.sh to .gitignore (#1792)
#1791 removed config/tap-driver.sh from the repo, as ./autogen.sh adds it automatically.
The current PR prevents this file from being added to the untracked changes list when doing git status.
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index b63d4c851..4bcdbe54a 100644 --- a/.gitignore +++ b/.gitignore @@ -24,6 +24,7 @@ generated/ *.gcov /lcov/ /config/compile +/config/tap-driver.sh .cvc4_config config.reconfig *.swp |