---- docs/grub.cfg.orig 2013-11-10 19:25:04.959888566 +0000
-+++ docs/grub.cfg 2013-11-10 19:25:10.260104712 +0000
+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
@@ -14,8 +14,8 @@
# For booting GNU/Linux
menuentry "GNU/Linux" --id gnulinux {