Commit bba21ec30fcc603765b39c296fa6bf79b07c420c

Stefano Lattarini 2013-01-16T13:35:10

Merge branch 'texi-no-split-info' * texi-no-split-info: texi: no longer support split info files