From c4a3c98e32175831478e09ddebe6c301bbad6fe9 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Tue, 11 Dec 2018 13:01:12 +0100
Subject: Fix issue #9175 Windows: VST addon does not work if CompCert is also
 installed

---
 dev/build/windows/patches_coq/VST.patch | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100755 dev/build/windows/patches_coq/VST.patch

(limited to 'dev/build/windows/patches_coq/VST.patch')

diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
new file mode 100755
index 0000000000..2c8c46373f
--- /dev/null
+++ b/dev/build/windows/patches_coq/VST.patch
@@ -0,0 +1,15 @@
+diff --git a/Makefile b/Makefile
+index 4a119042..fdfac13e 100755
+--- a/Makefile
++++ b/Makefile
+@@ -76,8 +76,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 SSReflect
+ ifdef MATHCOMP
-- 
cgit v1.2.3