make sure that the user does not have a separate partition for /boot in the script grub-install.

This commit is contained in:
okuji committed 2000-01-08 08:42:54 +00:00
1 parent 4ca2160923
commit adcd2008e1
4 files changed
+32 -1

No files matched your search

+13 -1
View File
@@ -197,12 +197,24 @@ fi
# Get the root drive.
# For now, this uses the program `df' to get the device name, but is
# this really portable?
root_device=`df ${grubdir} | grep /dev/ | sed 's%.*\(/dev/[a-z0-9]*\).*%\1%'`
root_device=`df / | grep /dev/ | sed 's%.*\(/dev/[a-z0-9]*\).*%\1%'`
root_drive=`convert $root_device`
if test "x$root_drive" = x; then
exit 1
fi
# Check if the root directory exists in the same device as the grub
# directory.
grubdir_device=`df ${grubdir} | grep /dev/ | sed 's%.*\(/dev/[a-z0-9]*\).*%\1%'`
if test $grubdir_device != $root_device; then
# For now, cannot deal with this situation.
cat <<EOF 1&>2
For now, cannot deal with the situation that $grubdir does not exist
in the root device. Install GRUB manually instead.
EOF
exit 1
fi
# Copy the GRUB images to the GRUB directory.
rm -f ${grubdir}/stage1 ${grubdir}/stage2 ${grubdir}/*stage1_5
cp ${pkgdatadir}/stage1 ${pkgdatadir}/stage2 ${pkgdatadir}/*stage1_5 ${grubdir}