emergency push for make run

2023-10-10 07:24:56 +02:00 · 2023-10-10 07:24:56 +02:00 · 1868986249
parent 67a57c4339
commit 1868986249
1 changed files with 1 additions and 1 deletions
--- a/MAKE.bat
+++ b/MAKE.bat
@ -742,7 +742,7 @@ if not "!other!"=="" (

 if "!run!"=="yes" (
    set exename=hello.exe
-    if "!other!"=="" (
+    if not "!other!"=="" (
        for /f "tokens=*" %%a in ("!other!") do set exename=%%~na.exe
    )
    echo run !exename! !run_args!