* doc/dejagnu.texi (Global config file): Fix broken @node.
authorBen Elliston <bje@gnu.org>
Fri, 8 Apr 2016 00:10:33 +0000 (10:10 +1000)
committerBen Elliston <bje@gnu.org>
Fri, 8 Apr 2016 00:10:33 +0000 (10:10 +1000)
commitedc6bd72d9c74230cf4336db3ca57b5596729d61
tree5b719be348def9220a040b34d7bd4cc741ca8c4e
parenta5fe563337dd18f64a9e291764d6ddf16d681578
* doc/dejagnu.texi (Global config file): Fix broken @node.
(Local config file): Likewise.
Reported by Faraz Shahbazker.
ChangeLog
doc/dejagnu.texi