From 1868986249c44121183908b40ea86118752ac9f4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dominik=20Madar=C3=A1sz?= Date: Tue, 10 Oct 2023 07:24:56 +0200 Subject: [PATCH] emergency push for make run --- MAKE.bat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MAKE.bat b/MAKE.bat index 18d6a9e..f833bc7 100644 --- 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!