summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/.gitignore1
-rw-r--r--compiler/Makefile3
2 files changed, 4 insertions, 0 deletions
diff --git a/compiler/.gitignore b/compiler/.gitignore
new file mode 100644
index 00000000..8357dae7
--- /dev/null
+++ b/compiler/.gitignore
@@ -0,0 +1 @@
+charon
diff --git a/compiler/Makefile b/compiler/Makefile
new file mode 100644
index 00000000..ea179dd2
--- /dev/null
+++ b/compiler/Makefile
@@ -0,0 +1,3 @@
+.PHONY: all
+all:
+ @dune build