build: Use unversioned doc directory. Thanks, Vagrant!
authorJan Nieuwenhuizen <janneke@gnu.org>
Mon, 4 Nov 2019 22:54:30 +0000 (23:54 +0100)
committerJan Nieuwenhuizen <janneke@gnu.org>
Mon, 4 Nov 2019 22:54:30 +0000 (23:54 +0100)
commit6a5619de9a7ca11a7a704caba5b578564b071dbe
tree1c2743295cafaff2f873728879bd6bc52b024762
parent45427bc641c96c1ad27db147c9a33ea8ff5421da
build: Use unversioned doc directory. Thanks, Vagrant!

* configure (docdir): Drop version.  Fixes Debian lint error.
* configure.sh (docdir): Likewise.
configure
configure.sh