automatically generated by browser
authorClaus Gittinger <cg@exept.de>
Fri, 14 Jun 2013 16:36:50 +0200
changeset 12919 1540cd2f04cd
parent 12918 8c7513224616
child 12920 ebcd88f199ff
automatically generated by browser
Makefile.init
--- a/Makefile.init	Fri Jun 14 16:36:48 2013 +0200
+++ b/Makefile.init	Fri Jun 14 16:36:50 2013 +0200
@@ -8,7 +8,7 @@
 #
 # MACOSX caveat:
 #   as filenames are not case sensitive (in a default setup),
-#   we cannot use tha above trick. Therefore, this file is now named
+#   we cannot use the above trick. Therefore, this file is now named
 #   "Makefile.init", and you have to execute "make -f Makefile.init" to
 #   get the initial makefile.  This is now also done by the toplevel CONFIG
 #   script.