From 88608b517e3a3fb556155440a4e2908b414c9826 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 3 Feb 2022 22:53:54 +0100
Subject: Make minor modifications

---
 Makefile | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 3227e0eb..3c9d9f1e 100644
--- a/Makefile
+++ b/Makefile
@@ -17,7 +17,8 @@ build-run:
 build-run-check-trace: generate-cfim
 	dune build src/main.exe && \
 	dune exec src/main.exe $(CFIM_TEST_FILE) > tests/trace_current.txt && \
-	cmp tests/trace_reference.txt tests/trace_current.txt
+	cmp tests/trace_reference.txt tests/trace_current.txt && \
+        cp fstar/Primitives.fst $(CHARON_TESTS_DIR)
 
 # Build the project and update the trace
 .PHONY: regen-trace
@@ -25,7 +26,8 @@ regen-trace: generate-cfim
 	dune build src/main.exe && \
 	dune exec src/main.exe $(CFIM_TEST_FILE) > tests/trace_current.txt && \
         rm -f tests/trace_reference.txt && \
-	cp tests/trace_current.txt tests/trace_reference.txt
+	cp tests/trace_current.txt tests/trace_reference.txt \
+        cp fstar/Primitives.fst $(CHARON_TESTS_DIR)
 
 .PHONY: generate-cfim
 generate-cfim:
-- 
cgit v1.2.3