Merge branch 'maint'
authorAndre Noll <maan@tuebingen.mpg.de>
Sat, 31 Dec 2016 20:12:33 +0000 (21:12 +0100)
committerAndre Noll <maan@tuebingen.mpg.de>
Sat, 31 Dec 2016 20:12:33 +0000 (21:12 +0100)
commit94802b02fadd65ac1704fe9fcbcf0a2b023d2fa4
tree1dc406b6151c7d33b055137c08244daac2578aa9
parent21c6e0b09b42e61e72b741bd726856ab0bcd1d64
parent191e65bdb00536514b8051b6d8e5b4d6772e948f
Merge branch 'maint'

A trivial conflict in configure.ac and remove/modify conflicts in
web/index.in.html and NEWS. The last file has been renamed to NEWS.md
in master. The conflict was resolved by copying the new text of the
NEWS file from maint (the release notes for v0.4.14) to NEWS.md and
to adjust the formatting to markdown syntax.
NEWS.md