aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorRogério Brito <rbrito@ime.usp.br>2011-12-08 13:18:17 -0200
committerRogério Brito <rbrito@ime.usp.br>2011-12-08 13:18:29 -0200
commit66e8777769ae1408dde499701e07e2bf2c598a21 (patch)
tree62a7830b4d3601b50b0c9cb5744eeba189fe6e51 /Makefile
parent348486ced4832e4de28c1eb024ef5d4f9c5e6fa5 (diff)
Makefile: Don't use `echo`'s `-e` option for portability.
Many systems (including Debian, Ubuntu and derivatives like Linux Mint) use Dash as a noninteractive version of `/bin/sh`, invoked by `make`. Dash's `echo` command doesn't understand the `-e` option and this generates spurious output when running `make`. See [a bugreport][0] for one of the many instances of this bug/feature in action. [0]: https://bugs.launchpad.net/ubuntu/+source/dash/+bug/72167
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile6
1 files changed, 4 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 07cc1eff7..b1a41079a 100644
--- a/Makefile
+++ b/Makefile
@@ -10,9 +10,11 @@ update-readme:
header=$$(sed -e '/.*## OPTIONS/,$$ d' README.md) && \
footer=$$(sed -e '1,/.*## FAQ/ d' README.md) && \
echo "$${header}" > README.md && \
- echo -e '\n## OPTIONS' >> README.md && \
+ echo >> README.md && \
+ echo '## OPTIONS' >> README.md && \
echo "$${options}" >> README.md&& \
- echo -e '\n## FAQ' >> README.md && \
+ echo >> README.md && \
+ echo '## FAQ' >> README.md && \
echo "$${footer}" >> README.md
compile: