summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon HO2022-09-22 16:25:30 +0200
committerGitHub2022-09-22 16:25:30 +0200
commit0227077e343a6243a5c69dfb3eb07f50006eb5ea (patch)
treef9c1c0187bd8ca7e399f353755eef44176cf42ca
parente7f76a4e46f24f54e5b49efee40e33e11128f49c (diff)
Update Makefile
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index aba2a67b..80cdad30 100644
--- a/Makefile
+++ b/Makefile
@@ -32,7 +32,7 @@ build:
test: build trans-no_nested_borrows trans-paper \
trans-hashmap trans-hashmap_main \
trans-external trans-constants \
- trans-nll-betree_nll trans-nll-betree_main \
+ trans-nll-betree_nll trans-nll-betree_main
# Verify the F* files generated by the translation
.PHONY: verify