From b9df6029cde75fd74b8752ec8196e2926e794e6f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Kr=C3=B6g?= Date: Mon, 21 Oct 2024 19:46:59 +0200 Subject: [PATCH] Die when PHP doc not found in update-property-map.php --- bin/stubs/update-property-map.php | 1 + 1 file changed, 1 insertion(+) diff --git a/bin/stubs/update-property-map.php b/bin/stubs/update-property-map.php index 115bc01f912..95d45d4f158 100755 --- a/bin/stubs/update-property-map.php +++ b/bin/stubs/update-property-map.php @@ -52,6 +52,7 @@ if (false === $docDir) { echo 'PHP doc not found!' . PHP_EOL; echo 'Please execute: git clone git@github.com:php/doc-en.git ' . dirname(__DIR__) . '/build/doc-en'; + die(1); } $files = new RegexIterator(