-diff -ur grub-2.04.orig/docs/grub.cfg grub-2.04/docs/grub.cfg
---- grub-2.04.orig/docs/grub.cfg 2019-08-18 15:56:16.561000000 +0200
-+++ grub-2.04/docs/grub.cfg 2019-08-18 15:56:54.745000000 +0200
+--- docs/grub.cfg.orig 2013-11-10 19:25:04.959888566 +0000
++++ docs/grub.cfg 2013-11-10 19:25:10.260104712 +0000
@@ -14,8 +14,8 @@
# For booting GNU/Linux
menuentry "GNU/Linux" --id gnulinux {