build: Fix for handling missing makeinfo.
authorJan Nieuwenhuizen <janneke@gnu.org>
Sat, 21 Jul 2018 09:19:55 +0000 (11:19 +0200)
committerJan Nieuwenhuizen <janneke@gnu.org>
Sat, 21 Jul 2018 09:19:55 +0000 (11:19 +0200)
commitd769a3d3c12adb4ac01c97eee94b41d8faf3a2f5
tree560994003e06ad1bb7ac4ddf5878df74f9efffa0
parent59c56ac72dd51564ff32761baab4a9a5698ef32d
build: Fix for handling missing makeinfo.

* configure (main): Update MAKEINFO.
configure