diff --git a/doc/build-html.bat b/doc/build-html.bat new file mode 100644 index 0000000..4c64977 --- /dev/null +++ b/doc/build-html.bat @@ -0,0 +1,35 @@ +@echo off +setlocal EnableExtensions + +set "SCRIPT_DIR=%~dp0" +set "SOURCE_FILE=%SCRIPT_DIR%index.html" +set "BUILD_DIR=%SCRIPT_DIR%build" +set "OUTPUT_FILE=%BUILD_DIR%\index.html" + +if not exist "%SOURCE_FILE%" ( + echo [ERROR] Source file not found: + echo %SOURCE_FILE% + exit /b 1 +) + +if not exist "%BUILD_DIR%" ( + mkdir "%BUILD_DIR%" + if errorlevel 1 ( + echo [ERROR] Cannot create build directory: + echo %BUILD_DIR% + exit /b 2 + ) +) + +copy /Y "%SOURCE_FILE%" "%OUTPUT_FILE%" >nul +if errorlevel 1 ( + echo [ERROR] Cannot build HTML. + exit /b 3 +) + +for %%F in ("%OUTPUT_FILE%") do set "OUTPUT_SIZE=%%~zF" +echo [OK] HTML documentation rebuilt: +echo %OUTPUT_FILE% +echo %OUTPUT_SIZE% bytes + +exit /b 0