[m-dev.] mercury-srcdist-rotd-2023-11-08 problem

[Peter Wang]

Hi,

There's something wrong with mercury-srcdist-rotd-2023-11-08.tar.{gz,xz}
Compared to the previous ROTD, the grade_lib/choose_grade.dv is missing
some list elements:

diff --git a/mercury-srcdist-rotd-2023-11-06/grade_lib/choose_grade.dv b/mercury-srcdist-rotd-2023-11-08/grade_lib/choose_grade.dv
index 7ea49b9..c0d5264 100644
--- a/mercury-srcdist-rotd-2023-11-06/grade_lib/choose_grade.dv
+++ b/mercury-srcdist-rotd-2023-11-08/grade_lib/choose_grade.dv
@@ -8,49 +8,21 @@
 choose_grade.ms = \
 	choose_grade.m \
 	grade_lib.m \
-	grade_setup.m \
-	grade_solver.m \
-	grade_spec.m \
-	grade_state.m \
-	grade_string.m \
-	grade_structure.m \
-	grade_vars.m \
 	var_value_names.m
 
 choose_grade.dep_errs = \
 	choose_grade.dep_err \
 	grade_lib.dep_err \
-	grade_setup.dep_err \
-	grade_solver.dep_err \
-	grade_spec.dep_err \
-	grade_state.dep_err \
-	grade_string.dep_err \
-	grade_structure.dep_err \
-	grade_vars.dep_err \
 	var_value_names.dep_err
 
 choose_grade.errs = \
 	choose_grade.err \
 	grade_lib.err \
-	grade_setup.err \
-	grade_solver.err \
-	grade_spec.err \
-	grade_state.err \
-	grade_string.err \
-	grade_structure.err \
-	grade_vars.err \
 	var_value_names.err
 
 choose_grade.mods = \
 	choose_grade \
 	grade_lib \
-	grade_lib.grade_setup \
-	grade_lib.grade_solver \
-	grade_lib.grade_spec \
-	grade_lib.grade_state \
-	grade_lib.grade_string \
-	grade_lib.grade_structure \
-	grade_lib.grade_vars \
 	var_value_names
 
 choose_grade.parent_mods = grade_lib

Peter