diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-27 18:28:42 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-27 18:28:42 -0500 |
| commit | 24a44a8723895a6749706ba2a3f73c51aea13d72 (patch) | |
| tree | 0ef895d3b91c3f9550b0374304b2bdbddeba9edb | |
| parent | dc21bb1de3dfe956312fe5ab734be8d59ee30135 (diff) | |
Ignore config/compile file, which newer autotools create
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index ea21c49bc..741f08ccd 100644 --- a/.gitignore +++ b/.gitignore @@ -23,6 +23,7 @@ generated/ \#*\# *.gcov /lcov/ +/config/compile .cvc4_config config.reconfig *.swp |