summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2024-04-03 17:36:05 +0200
committerSon Ho2024-04-03 17:36:05 +0200
commit3fdb4ca62155b6d913bceb7797ee9e10263cb087 (patch)
treefcdea76e394d5e5c747973e4176ba74fceb85b93 /Makefile
parent944a46fe61018e2b4266f19297daa822b41cf9e7 (diff)
Remove the check for CHARON_HOME
Diffstat (limited to '')
-rw-r--r--Makefile4
1 files changed, 0 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 3b44e0e6..1266e631 100644
--- a/Makefile
+++ b/Makefile
@@ -20,10 +20,6 @@ REGEN_LLBC ?=
# The path to Charon
CHARON_HOME ?= ../charon
-ifeq (,$(wildcard $(CHARON_HOME)))
- $(error The directory $$CHARON_HOME does not exist$(newline)(CHARON_HOME=$(CHARON_HOME)).)
-endif
-
# The paths to the test directories in Charon (Aeneas will look for the .llbc
# files in there).
CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests