diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-08 19:38:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-08 19:46:21 +0200 |
| commit | 51d38d0892eae4a253356e52614da6dee6513e9e (patch) | |
| tree | bbc7133c7aeef42c0c6d3d1548681f1f4951cde1 /test-suite/Makefile | |
| parent | 221f5e5622c866d1dae8e5c5e73156fa3e99ccfc (diff) | |
Removing dead code relative to the XML plugin.
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 20 |
1 files changed, 1 insertions, 19 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 81a556671..0f7abb78e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -346,25 +346,7 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -misc: misc/xml.log misc/deps-order.log misc/universes.log - -# Test xml compilation -xml: misc/xml.log -misc/xml.log: - @echo "TEST misc/xml" - $(HIDE){ \ - echo $(call log_intro,xml); \ - rm -rf misc/xml; \ - COQ_XML_LIBRARY_ROOT=misc/xml \ - $(bincoqc) -xml misc/berardi_test 2>&1; times; \ - if [ ! -d misc/xml ]; then \ - echo $(log_failure); \ - echo " misc/xml... failed"; \ - else \ - echo $(log_success); \ - echo " misc/xml...apparently ok"; \ - fi; rm -rf misc/xml; \ - } > "$@" +misc: misc/deps-order.log misc/universes.log # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R |