Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 88236a24 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Do no longer play tricks with headers of Coq realizations.

parent eeeb58d9
......@@ -1022,7 +1022,7 @@ ifeq (@enable_coq_fp_libs@,yes)
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
endif
update-coq: remove-coq-headers update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float headers-coq
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
......@@ -2044,23 +2044,16 @@ dist: $(MORE_DIST)
# file headers
###############
headers: headers-coq
headers:
headache -c misc/headache_config.txt -h misc/header.txt \
Makefile.in configure.in \
src/*/*.ml src/*/*.ml[iyl4] \
plugins/*/*.ml plugins/*/*.ml[ily] \
lib/coq-tactic/*.v lib/coq/*.v \
lib/coq-tactic/*.v lib/coq/*.v lib/coq/*/*.v \
src/server/*.c src/server/*.h \
src/ide/resetgc.c \
examples/use_api/*.ml
headers-coq:
headache -c misc/headache_config.txt -h misc/header.txt \
lib/coq/*/*.v
remove-coq-headers:
headache -r -c misc/headache_config.txt lib/coq/*/*.v
#########
# myself
#########
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment