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 /Makefile.extr | |
| parent | 1530f96aa259f346f235de713ab53b682b6d82f6 (diff) | |
| download | compcert-414225093054f0fdd9222e0ba9fbb95d345f5457.tar.gz compcert-414225093054f0fdd9222e0ba9fbb95d345f5457.zip | |
Update git ignore spec
ignore generated directory additional_files
Bug 20000
Diffstat (limited to 'Makefile.extr')
0 files changed, 0 insertions, 0 deletions