Rename batch file.
diff --git a/Doc/builddoc.bat b/Doc/make.bat
similarity index 100%
rename from Doc/builddoc.bat
rename to Doc/make.bat