[patch] \`default\' TYPO fix.

grub_set_default_TYPO.patch (text/plain), 731 bytes, created by Claudio Roberto França Pereira on 2011-12-05 00:42:34 UTC

--- util/grub-set-default.in	2004-07-16 08:44:57.000000000 -0300
+++ util/grub-set-default.in.new	2011-12-04 21:48:35.037095420 -0200
@@ -35,7 +35,7 @@
   -v, --version           print the version information and exit
   --root-directory=DIR    Use the directory DIR instead of the root directory
 
-ENTRY is a number or the special keyword \`default\'.
+ENTRY is a number or the special keyword \`default\`.
 
 Report bugs to <[e-mail]>.
 EOF
@@ -106,7 +106,7 @@
 #
 #
 # WARNING: If you want to edit this file directly, do not remove any line
-# from this file, including this warning. Using \`grub-set-default\' is
+# from this file, including this warning. Using \`grub-set-default\` is
 # strongly recommended.
 EOF