aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-10-16 15:52:19 +0200
committerCyril SIX <cyril.six@kalray.eu>2020-10-16 15:52:19 +0200
commitae3e1ed0515236e25924b12d475bc991a33b7632 (patch)
tree154428527771fbdec77f23846652d252400f81c8 /configure
parentfae36491fa22adaaf447e189988848483eb01dcd (diff)
parent53544f625ac6ed6ddb000f5ae8f28faac0da7a7b (diff)
downloadcompcert-kvx-ae3e1ed0515236e25924b12d475bc991a33b7632.tar.gz
compcert-kvx-ae3e1ed0515236e25924b12d475bc991a33b7632.zip
Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verif
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure6
1 files changed, 4 insertions, 2 deletions
diff --git a/configure b/configure
index adb81b56..b933f5da 100755
--- a/configure
+++ b/configure
@@ -689,12 +689,14 @@ echo "-R lib compcert.lib \
-R common compcert.common \
-R ${arch} compcert.${arch} \
-R backend compcert.backend \
+-R scheduling compcert.scheduling \
-R cfrontend compcert.cfrontend \
-R driver compcert.driver \
-R flocq compcert.flocq \
-R exportclight compcert.exportclight \
-R cparser compcert.cparser \
--R MenhirLib compcert.MenhirLib" > _CoqProject
+-R MenhirLib compcert.MenhirLib
+-R Impure lib.Impure" > _CoqProject
case $arch in
x86)
echo "-R x86_${bitsize} compcert.x86_${bitsize}" >> _CoqProject
@@ -840,7 +842,7 @@ fi
if [ "$arch" = "kvx" ]; then
cat >> Makefile.config <<EOF
-ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure
+ARCHDIRS=$arch $arch/lib $arch/abstractbb
EXECUTE=kvx-cluster --syscall=libstd_scalls.so --
CFLAGS= -D __KVX_COS__
SIMU=kvx-cluster --