diff options
| author | Maxime Dénès | 2019-07-22 09:34:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-07-22 09:34:15 +0200 |
| commit | 8ccafba4844c16ac4668bcb8475f3fb1d69c28ca (patch) | |
| tree | 959f41196339a8516ca6b0dec693d66d8016e991 /dev/build/windows/patches_coq/VST.patch | |
| parent | cd6fc50854285f02bf151e94bdfb819988531fd2 (diff) | |
| parent | 7341d286d4a9b440810097352fe257e476a8903c (diff) | |
Merge PR #10522: Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)
Reviewed-by: vbgl
Diffstat (limited to 'dev/build/windows/patches_coq/VST.patch')
| -rw-r--r-- | dev/build/windows/patches_coq/VST.patch | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch index 2c8c46373f..d047eb107f 100644 --- a/dev/build/windows/patches_coq/VST.patch +++ b/dev/build/windows/patches_coq/VST.patch @@ -1,8 +1,7 @@ diff --git a/Makefile b/Makefile -index 4a119042..fdfac13e 100755 --- a/Makefile +++ b/Makefile -@@ -76,8 +76,8 @@ endif +@@ -82,8 +82,8 @@ endif COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND) @@ -10,6 +9,6 @@ index 4a119042..fdfac13e 100755 -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 + # for ITrees + ifeq ($(wildcard InteractionTrees/the?ries),"InteractionTrees/theories") + EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree |
