Two small issues with make micro_release

[mezzarobba]

A trivial patch to experiment with the git workflow...

• the micro_release rule of the Makefile used |&, which is a bash4-ism
• the filtering of error messages did not work in non-English locales

Component: build

Reviewer: Marc Mezzarobba, Volker Braun

Issue created by migration from https://trac.sagemath.org/ticket/14908

[ohanar]

comment:2

The working branch was a workaround until #14781 got resolved.

Please rebase against the build_system branch.

[mezzarobba]

comment:3

Replying to @ohanar:

Please rebase against the build_system branch.

Done.

[vbraun]

Reviewer: Volker Braun

[vbraun]

comment:5

Looks good to me

[ohanar]

comment:6

I've merged this into the build_system branch at #14480, so I'm marking this as a duplicate so that we can close this ticket now.

[mezzarobba]

Changed branch from u/mmezzarobba/fix_micro_release to none

[mezzarobba]

comment:7

Replying to @ohanar:

I've merged this into the build_system branch at #14480, so I'm marking this as a duplicate so that we can close this ticket now.

Ok, so I've deleted the branch and filled in the Commit field instead.

[mezzarobba]

Commit: 0628ee3

[jdemeyer]

Changed commit from 0628ee3 to none

[jdemeyer]

Changed reviewer from Volker Braun to Marc Mezzarobba, Volker Braun

[jdemeyer]

Changed author from Marc Mezzarobba to none