Makefile.init
changeset 3473 4b3a14b23b8a
parent 3253 39e1a7bd62e9
equal deleted inserted replaced
3472:2d70c55d024f 3473:4b3a14b23b8a
     6 # My only task is to generate the real makefile and call make again.
     6 # My only task is to generate the real makefile and call make again.
     7 # Thereafter, I am no longer used and needed.
     7 # Thereafter, I am no longer used and needed.
     8 #
     8 #
     9 # MACOSX caveat:
     9 # MACOSX caveat:
    10 #   as filenames are not case sensitive (in a default setup),
    10 #   as filenames are not case sensitive (in a default setup),
    11 #   we cannot use tha above trick. Therefore, this file is now named
    11 #   we cannot use the above trick. Therefore, this file is now named
    12 #   "Makefile.init", and you have to execute "make -f Makefile.init" to
    12 #   "Makefile.init", and you have to execute "make -f Makefile.init" to
    13 #   get the initial makefile.  This is now also done by the toplevel CONFIG
    13 #   get the initial makefile.  This is now also done by the toplevel CONFIG
    14 #   script.
    14 #   script.
    15 
    15 
    16 .PHONY: run
    16 .PHONY: run