diff options
| author | Maxime Dénès | 2019-01-17 16:49:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-17 16:49:13 +0100 |
| commit | 2e231b0eb3d107aedc7a26dc173d6ac00cb3473f (patch) | |
| tree | 05caa777a0e233bd47b603fd109f4318f076f637 /dev/build/windows/patches_coq | |
| parent | f50256c7b4a75a59bb25a78431f0b24ae1046bf3 (diff) | |
| parent | 393f21c30921de34d48b751f6d8d50758982be4c (diff) | |
Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/build/windows/patches_coq')
| -rwxr-xr-x | dev/build/windows/patches_coq/VST.patch | 15 |
1 files changed, 15 insertions, 0 deletions
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 |