build: configure: Make dot optional.
authorJan Nieuwenhuizen <janneke@gnu.org>
Sun, 18 Nov 2018 13:30:47 +0000 (14:30 +0100)
committerJan Nieuwenhuizen <janneke@gnu.org>
Sun, 18 Nov 2018 13:30:47 +0000 (14:30 +0100)
commit3c9274ce2d40d9935a6ad5d9b6e2941e68674a75
tree8fe8d3469d8d94867697ed8b8500c85ae0e2096f
parent08f04f559670d9e8f57eb03bb9b13f4d0b81cedf
build: configure: Make dot optional.

* configure: Make dot optional.
configure