From 10ff9869f90e1b3afa86e42cffded53e7a4fbf7d Mon Sep 17 00:00:00 2001 From: ralf Date: Thu, 18 Jan 2024 22:13:49 +0200 Subject: [PATCH] if docs site directory exists, keep it updated --- install-cli.php | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/install-cli.php b/install-cli.php index e0b23c66b7..12f5185891 100755 --- a/install-cli.php +++ b/install-cli.php @@ -311,6 +311,12 @@ if ($npm) run_cmd($npm .' run build', 'rollup (npm run build)'); } +// if docs site directory exists, keep it updated +if ($npm && file_exists(__DIR__.'/docs/dist/site')) +{ + run_cmd($npm .' run docs', 'build docs (npm run docs)'); +} + echo "\n$succeeded tasks successful run". ($failed ? ', '.count($failed).' failed: '.implode(', ', $failed) : '')."\n\n"; exit(count($failed));