From ebc3dc20ce028a395377d74aad628cb12f58078f Mon Sep 17 00:00:00 2001 From: Paolo Tormene Date: Mon, 11 Mar 2024 16:08:16 +0100 Subject: [PATCH] Check differently if it is a pull request --- .github/workflows/demos_ltr_latest.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/demos_ltr_latest.yml b/.github/workflows/demos_ltr_latest.yml index 18bff1e60e90..fbfa1d19976d 100644 --- a/.github/workflows/demos_ltr_latest.yml +++ b/.github/workflows/demos_ltr_latest.yml @@ -15,7 +15,6 @@ jobs: demos: runs-on: ubuntu-latest env: - GITHUB_IS_PULL_REQUEST: ${{ github.event_name == 'pull_request' }} GITHUB_PULL_REQUEST: ${{ github.event.number }} GITHUB_DEF_BR: ${{ github.event.repository.default_branch }} GITHUB_REF: ${{ github.ref }} @@ -45,7 +44,7 @@ jobs: # GITHUB_DEF_BR: ${{ github.event.repository.default_branch }} # GITHUB_REF: ${{ github.ref }} run: | - if [ "$GITHUB_IS_PULL_REQUEST" ] + if ${{ github.event_name == 'pull_request' }} then echo "It is a pull request; use the corresponding branch: ${GITHUB_HD_REF}" python install.py devel --version ${GITHUB_HD_REF} @@ -71,7 +70,7 @@ jobs: oq dump /tmp/oqdata.zip oq restore /tmp/oqdata.zip /tmp/oqdata helpers/zipdemos.sh $(pwd)/demos - if [ "$GITHUB_IS_PULL_REQUEST" ] + if ${{ github.event_name == 'pull_request' }} then echo "It is a pull request; use the corresponding branch: ${GITHUB_HD_REF}" GITHUB_BR=${GITHUB_HD_REF}