summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore5
m---------ostumake0
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