Makefile.init
author Jan Vrany <jan.vrany@fit.cvut.cz>
Mon, 23 Nov 2015 11:14:30 +0100
changeset 551 00ebb1b85f53
parent 229 ed94847e203e
permissions -rw-r--r--
Fixed CI scripts on Windows For an unknown reason, unzip on Windows reports status code 50 (presumably "the disk is (or was) full during extraction.") even if there's plenty of space. To workaround this, simply ignore status code 50 on Windows. Sigh.

#
# 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.
#
# MACOSX caveat:
#   as filenames are not case sensitive (in a default setup),
#   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.

.PHONY: run

run: makefile
	$(MAKE) -f makefile

#only needed for the definition of $(TOP)
include Make.proto

makefile: mf

mf:
	$(TOP)/rules/stmkmf