From 13c71c63e0feb44735a050aca89b7db8da1c984c Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
Date: Tue, 7 Nov 2023 11:48:59 -0300
Subject: [PATCH] Testing develop.yml

---
 .github/workflows/develop.yml | 58 ++++++++++++++++++-----------------
 1 file changed, 30 insertions(+), 28 deletions(-)

diff --git a/.github/workflows/develop.yml b/.github/workflows/develop.yml
index 64bc2f190a6..5017be4a670 100644
--- a/.github/workflows/develop.yml
+++ b/.github/workflows/develop.yml
@@ -3,40 +3,41 @@ on:
   push:
     branches:
       - 'develop'
+      - 'update-bencher '
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 
 jobs:
 
-  version-bump:
-    name: 'Version Bump'
-    runs-on: ubuntu-20.04
-    steps:
-      - name: 'Check out code'
-        uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
-          # fetch-depth 0 means deep clone the repo
-          fetch-depth: 0
-      - name: 'Update Version'
-        run: |
-          set -x
-          git config user.name devops
-          git config user.email devops@runtimeverification.com
-          git checkout -B master origin/master
-          old_develop="$(git merge-base origin/develop origin/master)"
-          new_develop="$(git rev-parse origin/develop)"
-          if git diff --exit-code ${old_develop} ${new_develop} -- package/version; then
-            git merge --no-edit origin/develop
-            ./package/version.sh bump
-          else
-            git merge --no-edit --strategy-option=theirs origin/develop
-          fi
-          ./package/version.sh sub
-          if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
-            git push origin master
-          fi
+  # version-bump:
+  #   name: 'Version Bump'
+  #   runs-on: ubuntu-20.04
+  #   steps:
+  #     - name: 'Check out code'
+  #       uses: actions/checkout@v3
+  #       with:
+  #         token: ${{ secrets.JENKINS_GITHUB_PAT }}
+  #         # fetch-depth 0 means deep clone the repo
+  #         fetch-depth: 0
+  #     - name: 'Update Version'
+  #       run: |
+  #         set -x
+  #         git config user.name devops
+  #         git config user.email devops@runtimeverification.com
+  #         git checkout -B master origin/master
+  #         old_develop="$(git merge-base origin/develop origin/master)"
+  #         new_develop="$(git rev-parse origin/develop)"
+  #         if git diff --exit-code ${old_develop} ${new_develop} -- package/version; then
+  #           git merge --no-edit origin/develop
+  #           ./package/version.sh bump
+  #         else
+  #           git merge --no-edit --strategy-option=theirs origin/develop
+  #         fi
+  #         ./package/version.sh sub
+  #         if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
+  #           git push origin master
+  #         fi
 
   post-performance-tests:
     name: 'Performace Tests'
@@ -71,6 +72,7 @@ jobs:
             -e GITHUB_SHA=${GITHUB_SHA}                                        \
             --workdir /opt/workspace                                           \
             -v "${workspace}:/opt/workspace"                                   \
+            -v "${GITHUB_EVENT_PATH}:${GITHUB_EVENT_PATH}"                     \
             ${BASE_OS}:${BASE_DISTRO}
       - name: 'Setting up dependencies'
         run: |