Ne pas régénérer GRUB quand il est déjà configuré (#15)

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
+    # On commente la ligne d'origine, puis on ajoute les nôtres si elles
-    sed -i '/^GRUB_DEFAULT=0/ i#GRUB_DEFAULT=0\
+    # manquent. Les ajouter plutôt que les insérer règle deux choses : le
-    GRUB_DEFAULT=saved\
+    # fichier ne se retrouve plus avec des lignes indentées — GRUB les accepte,
-    GRUB_SAVEDEFAULT=true' /etc/default/grub
+    # 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
 }