summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 8 insertions, 0 deletions
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..5dfe960
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,8 @@
+AGDA ?= agda
+AGDALIB ?= /usr/share/agda-stdlib
+
+all:Everything.agdai
+clean:
+ rm -f *.agdai
+Everything.agdai:$(wildcard *.agda)
+ $(AGDA) -i. -i$(AGDALIB) Everything.agda