From 21549ffb6ec70ced134538a83b24ac98dcd7e068 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 28 Apr 2024 20:51:11 -0700 Subject: [PATCH 1/2] Improve clean target --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index f409e6d26e..3c85e02acd 100644 --- a/Makefile +++ b/Makefile @@ -38,6 +38,7 @@ clean-cache: # This target deletes files in the test cache. clean-test-cache: rm -rf cache-small + rm -f cache-small.tar # This target deletes files that are committed to version control. clean-stored-hashes: From 6ae7ec21d336b045dc81efc918dc126ef79ab56b Mon Sep 17 00:00:00 2001 From: Benedikt Schesch <37979523+benedikt-schesch@users.noreply.github.com> Date: Sun, 28 Apr 2024 21:02:51 -0700 Subject: [PATCH 2/2] Check for custom merge driver (#276) --- run.sh | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/run.sh b/run.sh index 2c3fb9ed92..bf66245c7a 100755 --- a/run.sh +++ b/run.sh @@ -55,6 +55,19 @@ done PATH=$(pwd)/src/scripts/merge_tools/:$PATH export PATH +echo "Checking for custom merge drivers in global configuration..." +merge_drivers=$(git config --global --get-regexp '^merge\..*\.driver$' || echo "No merge drivers set") + +if [ "$merge_drivers" == "No merge drivers set" ]; then + echo "No custom merge drivers found in global configuration. Proceeding with the evaluation." + # Include other commands to continue the script here +else + echo "Error: Custom merge drivers are set in global configuration." + echo "Please unset them before running the evaluation." + echo "Merge driver found: $merge_drivers" + exit 1 +fi + # Check if cache.tar exists and cache is missing if [ -f cache.tar ] && [ ! -d cache ]; then echo "Decompressing cache.tar"