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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
229
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     1
#
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     2
# DO NOT EDIT
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     3
#
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     4
# make uses this file (Makefile) only, if there is no
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     5
# file named "makefile" (lower-case m) in the same directory.
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     6
# My only task is to generate the real makefile and call make again.
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     7
# Thereafter, I am no longer used and needed.
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     8
#
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
     9
# MACOSX caveat:
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    10
#   as filenames are not case sensitive (in a default setup),
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    11
#   we cannot use the above trick. Therefore, this file is now named
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    12
#   "Makefile.init", and you have to execute "make -f Makefile.init" to
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    13
#   get the initial makefile.  This is now also done by the toplevel CONFIG
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    14
#   script.
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    15
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    16
.PHONY: run
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    17
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    18
run: makefile
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    19
	$(MAKE) -f makefile
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    20
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    21
#only needed for the definition of $(TOP)
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    22
include Make.proto
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    23
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    24
makefile: mf
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    25
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    26
mf:
ed94847e203e initial checkin
Claus Gittinger <cg@exept.de>
parents:
diff changeset
    27
	$(TOP)/rules/stmkmf