Bug#432156: 00_header long-winded

[Trent Buck]

Package: grub-pc
Version: 1.95+20070626-1
Severity: wishlist
File: /etc/grub.d/00_header
Tags: patch

The following is (AFAIK) SUS/POSIX portable, and is both terser and,
IMO, more concise:

| --- 00_header	2007/07/08 01:18:03	1.1
| +++ 00_header	2007/07/08 01:19:11	1.2
| @@ -25,20 +25,15 @@
|  # for convert_system_path_to_grub_path()
|  . ${libdir}/grub/update-grub_lib
|  
| -if [ "x${GRUB_DEFAULT}" = "x" ] ; then GRUB_DEFAULT=0 ; fi
| -if [ "x${GRUB_TIMEOUT}" = "x" ] ; then GRUB_TIMEOUT=5 ; fi
| -
| -cat << EOF
| -set default=${GRUB_DEFAULT}
| -set timeout=${GRUB_TIMEOUT}
| -EOF
| +echo set default="${GRUB_DEFAULT:=0}"
| +echo set timeout="${GRUB_TIMEOUT:=5}"
|  
| -if [ "x${GRUB_DRIVE}" = "x" ] ; then : ; else
| -  echo "set root=${GRUB_DRIVE}"
| +if test -n "$GRUB_DRIVE"
| +then echo set root="$GRUB_DRIVE"
|  fi
|  
| -if [ "x${GRUB_FONT_PATH}" = "x" ] ; then : ; else
| -  echo "font ${GRUB_FONT_PATH}"
| +if test -n "$GRUB_FONT_PATH"
| +then echo font "$GRUB_FONT_PATH"
|  fi
|  
|  case ${platform}:${GRUB_TERMINAL} in

Have a nice day.