tools/makeinfo_dummy

#!/bin/bash

# This is a stand-in for makeinfo, so that it's not required to build the
# tools, since we don't really need the docs.
# It emits 'texinfo 4.7' because configure looks for at least version 4.7.
echo "texinfo 4.7 dummy"