File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -652,6 +652,7 @@ stage0_new: .stage2.src.touch
652652 rm -rf " $( TO) /dune/libplugin" # idem
653653 rm -rf " $( TO) /dune/libapp" # we won't even build apps
654654 rm -rf " $( TO) /dune/tests" # we won't build tests
655+ rm -rf " $( TO) /karamel" # only needed in source packages
655656
656657bump-stage0 : stage0_new
657658 $(call bold_msg, "BUMP!")
@@ -669,6 +670,14 @@ bump-stage0: stage0_new
669670 sed -i ' s,include mk/generic-1.mk,include mk/generic-0.mk,' mk/fstar-01.mk
670671 rm -rf stage1
671672 cp -r stage2 stage1
673+ rm -rf stage1/dune/_build
674+ # Rename dune executables: stage1 must use fstarc1_*, not fstarc2_*
675+ sed -i ' s/fstarc2_/fstarc1_/g' stage1/dune/fstarc-bare/dune
676+ sed -i ' s/fstarc2_/fstarc1_/g' stage1/dune/fstarc-full/dune
677+ sed -i ' s/fstarc2_/fstarc1_/g' stage1/dune/tests/dune
678+ mv stage1/dune/fstarc-bare/fstarc2_bare.ml stage1/dune/fstarc-bare/fstarc1_bare.ml
679+ mv stage1/dune/fstarc-full/fstarc2_full.ml stage1/dune/fstarc-full/fstarc1_full.ml
680+ mv stage1/dune/tests/fstarc2_tests.ml stage1/dune/tests/fstarc1_tests.ml
672681 rm -f stage1/dune/fstar-guts/app
673682 ln -Trsf stage0/ulib/ml/app stage1/dune/fstar-guts/app
674683
You can’t perform that action at this time.
0 commit comments