Skip to content

Commit

Permalink
Testing script without git call
Browse files Browse the repository at this point in the history
  • Loading branch information
Robertorosmaninho committed Sep 21, 2023
1 parent 4704126 commit 92ebdcc
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 6 deletions.
4 changes: 0 additions & 4 deletions .github/workflows/develop.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 3 additions & 2 deletions k-distribution/tests/profiling/post_results_to_develop.py
Original file line number Diff line number Diff line change
Expand Up @@ -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/' \
Expand Down

0 comments on commit 92ebdcc

Please sign in to comment.