aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
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 /Makefile
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 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 5fc3997b..73b3a446 100644
--- a/Makefile
+++ b/Makefile
@@ -114,7 +114,7 @@ BACKEND=\
$(BACKENDLIB)
SCHEDULING= \
- RTLpathLivegenproof.v RTLpathSE_impl_junk.v \
+ RTLpathLivegenproof.v RTLpathSE_simu_specs.v \
RTLpathLivegen.v RTLpathSE_impl.v \
RTLpathproof.v RTLpathSE_theory.v \
RTLpathSchedulerproof.v RTLpath.v \