diff options
| -rw-r--r-- | .gitignore | 5 | ||||
| m--------- | ostumake | 0 |
2 files changed, 5 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..059891a --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +*.cmi +*.cmo +*.o +.Makefile.dep +tamasheq diff --git a/ostumake b/ostumake -Subproject 638d2159485e3605f5482aeda90506025a9f4d0 +Subproject c773c7c471d3614f0b1ae91a67f6a85f0584331 |
