adjust make.bat

main
Dominik Madarász 2023-09-11 13:42:52 +02:00
parent 1546a56a4a
commit 5747b95739
1 changed files with 2 additions and 1 deletions

View File

@ -129,8 +129,8 @@ rem generate prior files to a git release
if "%1"=="git" ( if "%1"=="git" (
rem call make.bat dll rem call make.bat dll
call make.bat prep call make.bat prep
call make.bat docs
call make.bat bind call make.bat bind
rem call make.bat docs
call make.bat amalgamation call make.bat amalgamation
call make.bat split call make.bat split
@ -161,6 +161,7 @@ if "%1"=="push" (
if "%2"=="out" ( if "%2"=="out" (
git push git push
) )
call make.bat vps
exit /b exit /b
) )