aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-10-17 15:43:14 +0200
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-10-17 15:43:14 +0200
commitdb3183cacb132d7153f653e2c3ae20b92ddfc03c (patch)
treec8a756d36267abd3349cec82c1f4daadff083371 /configure
parentae3e1ed0515236e25924b12d475bc991a33b7632 (diff)
downloadcompcert-kvx-db3183cacb132d7153f653e2c3ae20b92ddfc03c.tar.gz
compcert-kvx-db3183cacb132d7153f653e2c3ae20b92ddfc03c.zip
fixing the move of the verified prepass scheduler into scheduling/ directory
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure4
1 files changed, 1 insertions, 3 deletions
diff --git a/configure b/configure
index b933f5da..8ec92969 100755
--- a/configure
+++ b/configure
@@ -847,12 +847,10 @@ EXECUTE=kvx-cluster --syscall=libstd_scalls.so --
CFLAGS= -D __KVX_COS__
SIMU=kvx-cluster --
BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
- RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_simu_specs.v RTLpathSE_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\
Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
- AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\
- ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v
+ AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v
EOF
fi