aboutsummaryrefslogtreecommitdiff
path: root/dev/build/windows/patches_coq/VST.patch
blob: d047eb107fc9ddd9432d46c0fddc6ce1706003aa (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -82,8 +82,8 @@ endif

 COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND)

-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d))
-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d))
+COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d))
+EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d))
 # for ITrees
 ifeq ($(wildcard InteractionTrees/the?ries),"InteractionTrees/theories")
 EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree