Subject: [bug#72062] [PATCH 3/4] gnu: Add openmpi-5.

From: Ludovic Courtès <[email-masked]>
Date: Fri, 12 Jul 2024 10:42:47 +0200

Romain GARBAGE <[email-masked]> skribis:

> +(define-public openmpi-5

Also, probably as a separate patch, you could rename ‘openmpi’ to
‘openmpi-4’ and add:

  (define-public openmpi openmpi-4)

That way, we’ll only have to touch that variable when we decide to
upgrade wholesale.

WDYT?

Ludo’.