From d021905f3751c040824d4cd922ed136edd02efe6 Mon Sep 17 00:00:00 2001 From: Jef Roosens Date: Thu, 21 Apr 2022 16:12:37 +0200 Subject: [PATCH] chore: use -d dynamic_boehm for compilation --- Makefile | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index fb97ec2..c7f4384 100644 --- a/Makefile +++ b/Makefile @@ -3,13 +3,14 @@ SRC_DIR := src SOURCES != find '$(SRC_DIR)' -iname '*.v' V_PATH ?= v -V := $(V_PATH) -showcc -gc boehm +V := $(V_PATH) -showcc -gc boehm -d dynamic_boehm all: vieter # =====COMPILATION===== -# Regular binary +# We force the boehm gc to be compiled dynamically because otherwise, our CI +# build breaks. vieter: $(SOURCES) $(V) -g -o vieter $(SRC_DIR)