From 7772685dd72f9777fc9661db2c298d89e6286081 Mon Sep 17 00:00:00 2001
From: David Declerck <david.declerck@ocamlpro.com>
Date: Wed, 12 Jun 2024 16:18:51 +0200
Subject: [PATCH] Merge SVN 4026

---
 build_windows/makedist.cmd | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build_windows/makedist.cmd b/build_windows/makedist.cmd
index b3aada7b7..fb4006839 100644
--- a/build_windows/makedist.cmd
+++ b/build_windows/makedist.cmd
@@ -247,7 +247,7 @@ endlocal & exit /b %cb_errorlevel%
 
 :: pause if not started directly
 :pause_if_interactive
-if not [%stay_open%] == [] (
+if not [%stay_open%%CI%] == [] (
    echo.
    pause
 )