From 92ebdcc1958ace7c6cadb3e3ffa92074d1ca7121 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 21 Sep 2023 15:47:51 -0300 Subject: [PATCH] Testing script without git call --- .github/workflows/develop.yml | 4 ---- k-distribution/tests/profiling/post_results_to_develop.py | 5 +++-- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/.github/workflows/develop.yml b/.github/workflows/develop.yml index 771fcf5322d..bd3773aebbd 100644 --- a/.github/workflows/develop.yml +++ b/.github/workflows/develop.yml @@ -75,10 +75,6 @@ jobs: workspace=$(pwd) docker cp ${workspace}/. k-posting-profiling-tests-${GITHUB_SHA}:/opt/workspace - - name: 'Changing directory ownership' - run: | - docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c 'chown root:root /opt/workspace' - - name: 'Setting up dependencies' run: | set -euxo pipefail diff --git a/k-distribution/tests/profiling/post_results_to_develop.py b/k-distribution/tests/profiling/post_results_to_develop.py index f019a32d81e..5f5ae17bcb1 100755 --- a/k-distribution/tests/profiling/post_results_to_develop.py +++ b/k-distribution/tests/profiling/post_results_to_develop.py @@ -25,8 +25,9 @@ def execute_command(command): return result.stdout # git command to get the last commit in develop -commit_command = [ 'git', 'log', '--format=\"%H\"', '-n', '1' ] -COMMIT_SHA = execute_command(commit_command).strip('\"').strip('\"\n') +#commit_command = [ 'git', 'log', '--format=\"%H\"', '-n', '1' ] +COMMIT_SHA = "4704126b2a6e014d8787894a4d9f5efedbbcb204" +#execute_command(commit_command).strip('\"').strip('\"\n') # curl command to get the branch name of last commit in develop API_URL = 'https://api.github.com/repos/runtimeverification/k/commits/' \