diff options
Diffstat (limited to 'Makefile.config')
| -rw-r--r-- | Makefile.config | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Makefile.config b/Makefile.config index 0fa18a6466..dd05b54abf 100644 --- a/Makefile.config +++ b/Makefile.config @@ -69,6 +69,7 @@ RM ?= rm -f SCSH ?= scsh SED ?= sed SORT ?= sort +STAT ?= stat TAIL ?= tail TAR ?= tar TOUCH ?= touch @@ -88,6 +89,12 @@ PICO ?= pico PICO_FLAGS ?= -make -source 1.4 ############################################################################## +# XSLT processor + +XSLTPROC ?= xsltproc +XSLTPROC_FLAGS ?= + +############################################################################## # Makefile functions RUN ?= $(ECHO) '$(1)'; $(1) || exit $$? |