Oops: update the menu generation script.
Authored by: dominique_libre 2020-04-12
Parent: [r1035]
Child: [r1037]
