diff options
Diffstat (limited to 'users/wpcarro/scratch/compiler/.gitignore')
| -rw-r--r-- | users/wpcarro/scratch/compiler/.gitignore | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/users/wpcarro/scratch/compiler/.gitignore b/users/wpcarro/scratch/compiler/.gitignore index 25414be2a981..96261d3fc7e9 100644 --- a/users/wpcarro/scratch/compiler/.gitignore +++ b/users/wpcarro/scratch/compiler/.gitignore @@ -1,2 +1,5 @@ a.out -*.cmi \ No newline at end of file +*.cmi +*.cmo +*.cmx +*.o \ No newline at end of file |