summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorRobert Norton2016-04-14 12:11:41 +0100
committerRobert Norton2016-04-14 12:11:52 +0100
commitd97503d21f7f5921008fb22dbe823fa282f1b2b1 (patch)
tree5d7be687741838445a419516739e832793269be5 /src
parentf9345ad67348f715754a8d6aba9510fa55aeb74d (diff)
add cheri make target analagous to mips
Diffstat (limited to 'src')
-rw-r--r--src/Makefile2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Makefile b/src/Makefile
index c010b992..12535ace 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -64,6 +64,8 @@ run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_che
mips: elf run_mips.native
+cheri: elf run_cheri.native
+
clean:
-ocamlbuild -clean
-rm -rf _build *.native