File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -5,7 +5,7 @@ include visitors.mk
55
66FSTAR_EXE ?= fstar.exe
77
8- all : local-install krmllib
8+ all : local-install
99
1010# If we are just trying to do a minimal build, we don't need F*.
1111# Note: lazy assignment so this does not warn if fstar.exe is not there
@@ -19,6 +19,7 @@ minimal: lib/Version.ml
1919 dune build
2020 ln -sf _build/default/src/Karamel.exe krml
2121
22+ ifneq ($(LOWSTAR ) ,false)
2223krmllib : minimal
2324 @# Make sure krml can find its relevant directories, since
2425 @# it is not yet installed with them.
@@ -27,6 +28,9 @@ krmllib: minimal
2728 KRML_INCLUDEDIR=$(CURDIR ) /include \
2829 KRML_MISCDIR=$(CURDIR ) /misc \
2930 $(MAKE ) -C krmllib
31+ else
32+ krmllib : minimal
33+ endif
3034
3135# A full local install. out/ will contain essentially the same directory
3236# as an OPAM install or binary package.
You can’t perform that action at this time.
0 commit comments