diff options
Diffstat (limited to '')
| -rwxr-xr-x | doc/tools/texi2www/texi2www | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/tools/texi2www/texi2www b/doc/tools/texi2www/texi2www index dbce9a7f19..1a294d24bb 100755 --- a/doc/tools/texi2www/texi2www +++ b/doc/tools/texi2www/texi2www @@ -1020,6 +1020,11 @@ sub read_input "$texinfo_file[0] line $."); next; } + if (/^\@ifnottex/) { + &read_input($echo,'/^\@end\s+ifnottex/', + "$texinfo_file[0] line $."); + next; + } if (/^\@ifhtml/) { &read_input($echo,'/^\@end\s+ifhtml/', "$texinfo_file[0] line $."); |