Confusion between stdlib and stdlib-flambda when it fails

[SkySkimmer]

coq/coq#20215 (comment)

🏃 @coqbot ci minimize will minimize the following targets: ci-stdlib, ci-stdlib

[JasonGross]

As far as I can tell

bot/src/actions.ml

Lines 1007 to 1012 in e838d62

	let shorten_ci_check_name target =
	target
	|> Str.global_replace (Str.regexp "GitLab CI job") ""
	|> Str.global_replace (Str.regexp "(pull request)") ""
	|> Str.global_replace (Str.regexp "(branch)") ""
	|> Stdlib.String.trim

seems fine ... I'm trying to find/recall where the library: / plugin: bits get chopped off

[JasonGross]

The solution should be to just include + in

bot/src/actions.ml

Line 901 in e838d62

if string_match ~regexp:"\\([^: ]*\\):\\(ci-[A-Za-z0-9_-]*\\)" full_name

I don't have time to take care of & test this right now, unfortunately

[Zimmi48]

I don't think fixing this is as trivial as adding + to this regexp, because while the CI job is called ci-stdlib+flambda, the Makefile.ci target is ci-stdlib. So, we would need specific support for +flambda jobs (or +whatever jobs) for which we would be able to store a separate GitLab job name and Makefile.ci target.