Comment 2 for bug 289791

Revision history for this message
Agostino Russo (ago) wrote :

--- grub-installer-1.32ubuntu10/grub-installer 2008-10-20 23:04:58.000000000 +0100
+++ grub-installer 2008-10-27 15:58:35.000000000 +0000
@@ -978,13 +978,14 @@
        # Be careful to deal with either UUID-style or non-UUID-style groot.
        # grub4dos doesn't recognise UUIDs yet.
        sed -i "s:^\(# groot=\)[^(].*:\1():; s:^\(# groot=([^)]*)\).*:\1$bootdev_directory:" $ROOT/boot/grub/$menu_file
+ hide_menu=true
 fi
 # In either case, update the Debian kernel entries
 if [ "$user_params" ] || [ "$bootdev_directory" ]; then
        update_grub
 fi

-if [ -s /tmp/os-probed ]; then
+if [ -s /tmp/os-probed ] && [ "$hide_menu" != true ]; then
        # Other operating systems are installed, so show the menu by default
        # and raise the timeout.
        sed -i 's/^hiddenmenu[[:space:]]*$/#hiddenmenu/;