From f4973d593eaa7d3dd291c60034ba1ec213932e36 Mon Sep 17 00:00:00 2001
From: Richard Brooksby <rb@ravenbrook.com>
Date: Wed, 11 Jan 2023 13:46:53 +0000
Subject: [PATCH] Github ci's cmd exited right after the first line, so perhaps
 the run script is secretly a batch file and needs to use "call".

---
 mps/.github/workflows/c-cpp.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mps/.github/workflows/c-cpp.yml b/mps/.github/workflows/c-cpp.yml
index 1e743388e80..eb387ce0ad1 100644
--- a/mps/.github/workflows/c-cpp.yml
+++ b/mps/.github/workflows/c-cpp.yml
@@ -37,7 +37,7 @@ jobs:
     - name: make
       # Using path to Visual Studio documented at <https://github.com/actions/runner-images/blob/e6fcf60b8e6c0f80a065327eaefe836881c28b68/images/win/Windows2022-Readme.md?plain=1#L215>.
       run: |
-         "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" x64
+         call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" x64
          cd code
          nmake /f w3i6mv.nmk
       shell: cmd