#5444: adapt make.bat to new htmlhelp output file name.
1 file changed