diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/clightgen/Makefile | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/test/clightgen/Makefile b/test/clightgen/Makefile index bf4a044b..fdfbc3fb 100644 --- a/test/clightgen/Makefile +++ b/test/clightgen/Makefile @@ -5,8 +5,12 @@ ARCHDIRS=$(ARCH) else ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH) endif -RECDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight -COQINCLUDES=$(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) +RECDIRS := lib common $(ARCHDIRS) cfrontend exportclight +COQINCLUDES := $(foreach d, $(RECDIRS), -R ../../$(d) compcert.$(d)) +ifeq ($(LIBRARY_FLOCQ),local) +COQINCLUDES += -R ../../flocq Flocq +endif + CLIGHTGEN=../../clightgen COQC=coqc |