From ee0f12440ceb58a9e0388d112d6e0d34ce1ecb95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 4 Dec 2024 20:01:40 -0800 Subject: [PATCH] Makefiles: more conditional ocaml build, for package testing --- examples/Makefile | 4 ++++ examples/data_structures/Makefile | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/examples/Makefile b/examples/Makefile index 6a00a2ff1f1..97b5b907b26 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -40,7 +40,11 @@ SUBDIRS += verifythis # SUBDIRS_CLEAN += hello SUBDIRS_ALL += dependencies SUBDIRS_CLEAN += dependencies + +HAS_OCAML ?= 1 +ifneq (,$(HAS_OCAML)) SUBDIRS_ALL += native_tactics +endif SUBDIRS_CLEAN += native_tactics FSTAR_ROOT ?= .. diff --git a/examples/data_structures/Makefile b/examples/data_structures/Makefile index 0c9a1893327..3d83c7c748d 100644 --- a/examples/data_structures/Makefile +++ b/examples/data_structures/Makefile @@ -1,7 +1,11 @@ FSTAR_ROOT ?= ../.. include $(FSTAR_ROOT)/mk/test.mk +HAS_OCAML ?= 1 + +ifneq (,$(HAS_OCAML)) all: $(OUTPUT_DIR)/RBTreeIntrinsic_patched.exe +endif # EXTRACT = RBTreeIntrinsic