diff options
Diffstat (limited to 'test/.gitignore')
| -rw-r--r-- | test/.gitignore | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/.gitignore b/test/.gitignore new file mode 100644 index 00000000..09144e68 --- /dev/null +++ b/test/.gitignore @@ -0,0 +1,8 @@ +# CompCert-generated files +*.s +*.sdump +*.parsed.c +*.compcert.c +*.light.c +*.compcert +*.gcc |