diff --git a/code/linux/linux-mint/install.sh b/code/linux/linux-mint/install.sh index bb33d49..c67e8bc 100644 --- a/code/linux/linux-mint/install.sh +++ b/code/linux/linux-mint/install.sh @@ -337,11 +337,32 @@ configuration_apt() { # GRUB : sélection automatique de la dernière entrée utilisée # ############################################################### modif_grub() { + # Rien à faire si c'est déjà en place. + # + # update-grub lance os-prober, qui part sonder toutes les partitions de la + # machine à la recherche d'autres systèmes, puis régénère la configuration + # entière : vingt à trente secondes qu'on ne rattrape pas, et qu'on payait + # jusqu'ici à chaque exécution, y compris quand il n'y avait rien à + # changer. Sur une install party de quinze machines, cela se voit. + if grep -q '^GRUB_DEFAULT=saved' /etc/default/grub \ + && grep -q '^GRUB_SAVEDEFAULT=true' /etc/default/grub; then + echo -e "==> GRUB est déjà configuré, rien à changer\n" + return 0 + fi + echo -e "==> Modification de GRUB\n" - # On comment la ligne "GRUB_DEFAULT=0" et on ajoute les "bonnes" options - sed -i '/^GRUB_DEFAULT=0/ i#GRUB_DEFAULT=0\ - GRUB_DEFAULT=saved\ - GRUB_SAVEDEFAULT=true' /etc/default/grub + # On commente la ligne d'origine, puis on ajoute les nôtres si elles + # manquent. Les ajouter plutôt que les insérer règle deux choses : le + # fichier ne se retrouve plus avec des lignes indentées — GRUB les accepte, + # mais elles trompent la lecture quand on vient déboguer —, et la fonction + # fait toujours son travail lorsque « GRUB_DEFAULT=0 » a disparu, ce qui + # arrive dès qu'un autre outil est passé avant nous. + sed -i 's/^GRUB_DEFAULT=0/#&/' /etc/default/grub + grep -q '^GRUB_DEFAULT=saved' /etc/default/grub \ + || echo 'GRUB_DEFAULT=saved' >> /etc/default/grub + grep -q '^GRUB_SAVEDEFAULT=true' /etc/default/grub \ + || echo 'GRUB_SAVEDEFAULT=true' >> /etc/default/grub + # On met à jour GRUB update-grub }