change echo to printf (POSIX vs. GNU issue)

master
Benjamin Kellermann 9 years ago
parent a955a4f486
commit 2cdeece583
  1. 2
      Makefile

@ -47,7 +47,7 @@ CHECKPGFREALJOBNAME=true
#shut the make up
VERBOSE ?= @
PRINTF ?= echo -e
PRINTF ?= printf
# all extensions which should be deleted with make clean
TEXEXT=log aux toc synctex.gz synctex.gz\(busy\) pdfsync

Loading…
Cancel
Save