diff options
Diffstat (limited to '')
| -rw-r--r-- | examples/misc/Makefile | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/examples/misc/Makefile b/examples/misc/Makefile new file mode 100644 index 00000000..a8e3fbc6 --- /dev/null +++ b/examples/misc/Makefile @@ -0,0 +1,15 @@ +CHARON_HOME=../../../charon/charon + +all: build test translate + +.PHONY: build +build: + cargo build + +.PHONY: test +test: + cargo test + +.PHONY: translate +translate: + cd $(CHARON_HOME) && cargo run ../../aeneas/examples/misc/src/hashmap.rs |