diff -r c81148cde6d9 -r 8a5b7afa28ff Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Makefile Thu Aug 30 11:46:39 2012 +0000 @@ -0,0 +1,19 @@ +# +# DO NOT EDIT +# +# make uses this file (Makefile) only, if there is no +# file named "makefile" (lower-case m) in the same directory. +# My only task is to generate the real makefile and call make again. +# Thereafter, I am no longer used and needed. +# + +.PHONY: run + +run: makefile + $(MAKE) -f makefile + +#only needed for the definition of $(TOP) +include Make.proto + +makefile: + $(TOP)/rules/stmkmf