diff options
author | Markus Pister <pister@absint.com> | 2017-06-28 07:30:14 +0200 |
---|---|---|
committer | Markus Pister <pister@absint.com> | 2017-06-28 07:30:14 +0200 |
commit | 414225093054f0fdd9222e0ba9fbb95d345f5457 (patch) | |
tree | e0f3609b546c1f2792199ee0a80369c63098e32d | |
parent | 1530f96aa259f346f235de713ab53b682b6d82f6 (diff) | |
download | compcert-414225093054f0fdd9222e0ba9fbb95d345f5457.tar.gz compcert-414225093054f0fdd9222e0ba9fbb95d345f5457.zip |
Update git ignore spec
ignore generated directory additional_files
Bug 20000
-rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -27,6 +27,7 @@ _CoqProject # Generated files .depend .depend.extr +additional_files compcert.ini x86/ConstpropOp.v x86/SelectOp.v |