From 4347d18af528f64459cb2238bd915e0e29b1b45f Mon Sep 17 00:00:00 2001 From: Roi Klevansky Date: Mon, 14 Oct 2024 00:00:21 +0300 Subject: [PATCH] build: add script which patches GDB --- src/patch_gdb.sh | 51 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100755 src/patch_gdb.sh diff --git a/src/patch_gdb.sh b/src/patch_gdb.sh new file mode 100755 index 0000000..2699695 --- /dev/null +++ b/src/patch_gdb.sh @@ -0,0 +1,51 @@ +#!/bin/bash + +function apply_patch() { + # Apply a patch to a directory. + # + # Parameters: + # $1: directory + # $2: path of patch + # + # Returns: + # 0: success + # 1: failure + + local dir="$1" + local patch="$(realpath "$2")" + + pushd "$dir" > /dev/null + if [[ $? -ne 0 ]]; then + return 1 + fi + + # Check if the patch was already applied + if ! patch -p1 --dry-run < "$patch" &>/dev/null; then + >&2 echo "Error: patch already applied" + popd > /dev/null + return 1 + fi + + patch -p1 < "$patch" + if [[ $? -ne 0 ]]; then + popd > /dev/null + return 1 + fi + + popd > /dev/null +} + +function main() { + if [[ $# -ne 2 ]]; then + >&2 echo "Usage: $0 " + exit 1 + fi + + apply_patch "$1" "$2" + if [[ $? -ne 0 ]]; then + >&2 echo "Error: failed to apply GDB patch" + exit 1 + fi +} + +main "$@"