aboutsummaryrefslogtreecommitdiff
path: root/makefile
diff options
context:
space:
mode:
authorpacien2018-04-29 20:19:28 +0200
committerpacien2018-04-29 20:19:28 +0200
commit55f5d164762fc37fc53e6e94da2aa92d84e8c145 (patch)
treea4ffc86a7d22f893f4b0bf50fdc1677d816c017a /makefile
parent7d05d97c8e51e77f117fc14f060bb0c54b86a135 (diff)
parente828fbc45672ed2b6d9e78e6b667905d3c68267c (diff)
downloadurm-55f5d164762fc37fc53e6e94da2aa92d84e8c145.tar.gz
Merge branch 'eurm'
Diffstat (limited to 'makefile')
-rw-r--r--makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/makefile b/makefile
index 6345a40..6aceab8 100644
--- a/makefile
+++ b/makefile
@@ -7,6 +7,7 @@ SOURCES = \
7 instptr.mli instptr.ml \ 7 instptr.mli instptr.ml \
8 reg.mli reg.ml \ 8 reg.mli reg.ml \
9 urm.mli urm.ml urm_test.ml \ 9 urm.mli urm.ml urm_test.ml \
10 eurm.mli eurm.ml eurm_test.ml \
10 main.ml 11 main.ml
11 12
12OCAMLMAKEFILE = /usr/share/ocamlmakefile/OCamlMakefile 13OCAMLMAKEFILE = /usr/share/ocamlmakefile/OCamlMakefile