diff --git a/Makefile b/Makefile index 6dd87409e..e85f29b48 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,16 @@ # NOTE: this Makefile requires GNU make +### Defensive settings for make: +# https://tech.davis-hansson.com/p/make/ +SHELL := bash +.ONESHELL: +.SHELLFLAGS := -xeu -o pipefail -c +.SILENT: +.DELETE_ON_ERROR: +MAKEFLAGS += --warn-undefined-variables +MAKEFLAGS += --no-builtin-rules + default: @echo "no default target"