aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-11-07 18:27:45 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-11-07 18:27:45 +0100
commitdabd9ab46319ff93aa8451e033b3b37726a50f2c (patch)
tree9194caf9ed13dd2f77d835d4230eadb05135b54c
parentb9588e8f752e03aaae2a2f8f63447e0687b71bff (diff)
downloadcompcert-kvx-dabd9ab46319ff93aa8451e033b3b37726a50f2c.tar.gz
compcert-kvx-dabd9ab46319ff93aa8451e033b3b37726a50f2c.zip
do not test with picosat
-rw-r--r--test/Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/Makefile b/test/Makefile
index 2dd104d3..a846e93b 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -13,9 +13,10 @@ endif
all:
set -e; for i in $(DIRS); do $(MAKE) CCOMPOPTS='$(CCOMPOPTS)' -C $$i all; done
+ifneq ($(ARCH),kvx)
cd $(PICOSAT) && ./configure.sh && cd ..
$(MAKE) CCOMPOPTS='$(CCOMPOPTS)' -C $(PICOSAT) -f Makefile.local all
-
+endif
test:
set -e; for i in $(DIRS); do $(MAKE) SIMU='$(SIMU)' -C $$i test; done