2014-07-30 12:21:52 -05:00
|
|
|
|
2019-02-15 13:14:17 -06:00
|
|
|
# Don't bother defining default values for SEED and EXTRA_FLAGS.
|
|
|
|
# Their "natural" default values should be sufficient,
|
|
|
|
# and they may be overridden in the environment.
|
2016-09-15 03:00:29 -05:00
|
|
|
ifneq ($(strip $(SEED)),)
|
|
|
|
SEEDOPT=-S$(SEED)
|
|
|
|
endif
|
2014-07-30 12:21:52 -05:00
|
|
|
|
|
|
|
$(MAKECMDGOALS):
|
2016-09-15 03:00:29 -05:00
|
|
|
@$(basename $(MAKEFILE_LIST)).sh -G -j $(SEEDOPT) $(EXTRA_FLAGS) $@
|
2014-07-30 12:21:52 -05:00
|
|
|
|
|
|
|
.PHONY: $(MAKECMDGOALS)
|
|
|
|
|