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

[Julien Fischer]

On Fri, 10 Nov 2023, Peter Wang wrote:

> 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

That's really strange; I just tried building a source distribution using
the same compiler, rotd-2023-11-08, and choose_grade.dv is complete with that.

Julien.