summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2023-12-22 18:47:50 +0100
committerSon Ho2023-12-22 18:47:50 +0100
commit455ba366f9c8d07a1f1848ec0960b1f2d161e7cf (patch)
tree03493e0e2eddef8187296befceeda40eba102c4c /Makefile
parente799ef503dda30b6dcbecb042ecb0fae1a71fa81 (diff)
Update the library for F*
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile6
1 files changed, 4 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 2cce30d9..37408554 100644
--- a/Makefile
+++ b/Makefile
@@ -70,9 +70,11 @@ build-bin-dir: build-bin build-lib
mkdir -p bin
cp -f compiler/_build/default/main.exe bin/aeneas
cp -f compiler/_build/default/main.exe bin/aeneas.cmxs
- mkdir -p bin/backends/fstar
+ mkdir -p bin/backends/fstar/split
+ mkdir -p bin/backends/fstar/merge
mkdir -p bin/backends/coq
- cp -rf backends/fstar/*.fst* bin/backends/fstar/
+ cp -rf backends/fstar/split/*.fst* bin/backends/fstar/split/
+ cp -rf backends/fstar/merge/*.fst* bin/backends/fstar/merge/
cp -rf backends/coq/*.v bin/backends/coq/
.PHONY: doc