Skip to content

Commit

Permalink
Added correct gitconfig
Browse files Browse the repository at this point in the history
  • Loading branch information
Benedikt Schesch committed May 7, 2024
2 parents a3de058 + 1469c87 commit 6881407
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 11 deletions.
1 change: 1 addition & 0 deletions .github/workflows/check-reproducibility.yml
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ jobs:
run: |
git config --global user.email "[email protected]"
git config --global user.name "Example Example"
python3 src/python/replay_merge.py --idx 522-15 -delete_workdir
head -n 151 results/combined/result.csv > temp.csv && mv temp.csv results/combined/result.csv
make NUM_PROCESSES=1 check-merges-reproducibility
env:
Expand Down
2 changes: 0 additions & 2 deletions .github/workflows/small-test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,8 +56,6 @@ jobs:
- run: echo "LOGURU_COLORIZE=NO" >> $GITHUB_ENV
- name: Run small test
run: |
git config --global user.email "[email protected]"
git config --global user.name "Example Example"
git config --global merge.customMerge.name "Always incorrect custom merge driver"
git config --global merge.customMerge.driver 'fake-merge-driver %O %A %B %L %P'
make small-test
Expand Down
6 changes: 0 additions & 6 deletions run.sh
Original file line number Diff line number Diff line change
Expand Up @@ -57,12 +57,6 @@ export PATH

GIT_CONFIG_GLOBAL=$(pwd)/.gitconfig
export GIT_CONFIG_GLOBAL
if git config --list --show-origin | grep 'file:'"$GIT_CONFIG_GLOBAL" > /dev/null; then
echo "Error: Global config is not empty"
exit 1
else
echo "Global config is empty"
fi

# Check if cache.tar exists and cache is missing
if [ -f cache.tar ] && [ ! -d cache ]; then
Expand Down
6 changes: 3 additions & 3 deletions src/scripts/merge_tools/spork.sh
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,9 @@ branch1=$2
branch2=$3

# set up spork driver
(echo "[merge \"spork\"]";
echo " name = spork";
echo " driver = java -jar $spork_absolutepath --git-mode %A %O %B -o %A") >> "$clone_dir/.git/config"
git config --local merge.spork.name "spork"
git config --local merge.spork.driver "java -jar $spork_absolutepath --git-mode %A %O %B -o %A"

echo "*.java merge=spork" >> "$clone_dir/.gitattributes"

# perform merge
Expand Down

0 comments on commit 6881407

Please sign in to comment.