Fix build issues in Doc/make.bat (#3658)

1 file changed