[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

I just forced the build of rotd-2023-11-10. Its copy of
grade_lib/choose_grade.dv has the correct contents.  The only
explanation I can think of is that we build the source distribution
at -j8, which presumably includes the dependency step in the grade_lib
directory.  There are three targets in that directory; possibly there's
some conflict between them?

Julien.