From 957122efded6c57ddb4055aef916060364bca1cf Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 16 Jun 2021 10:23:14 +1000 Subject: [PATCH] Use bash instead of zsh --- run_all.sh | 2 +- run_original_chuffed.sh | 2 +- run_original_gecode.sh | 2 +- run_record_gecode.sh | 2 +- run_replay_gecode.sh | 2 +- run_restart_chuffed.sh | 2 +- run_restart_gecode.sh | 2 +- setup.sh | 2 +- 8 files changed, 8 insertions(+), 8 deletions(-) diff --git a/run_all.sh b/run_all.sh index d2622c6..c922af2 100755 --- a/run_all.sh +++ b/run_all.sh @@ -1,4 +1,4 @@ -#!/bin/zsh +#!/usr/bin/env bash trap "exit" INT set -e diff --git a/run_original_chuffed.sh b/run_original_chuffed.sh index 21f1dd4..7055f81 100755 --- a/run_original_chuffed.sh +++ b/run_original_chuffed.sh @@ -1,4 +1,4 @@ -#!/bin/zsh +#!/usr/bin/env bash trap "exit" INT set -e diff --git a/run_original_gecode.sh b/run_original_gecode.sh index c1d4441..73bc482 100755 --- a/run_original_gecode.sh +++ b/run_original_gecode.sh @@ -1,4 +1,4 @@ -#!/bin/zsh +#!/usr/bin/env bash trap "exit" INT set -e diff --git a/run_record_gecode.sh b/run_record_gecode.sh index 80390a5..24192f6 100755 --- a/run_record_gecode.sh +++ b/run_record_gecode.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env zsh +#!/usr/bin/env bash trap "exit" INT set -e diff --git a/run_replay_gecode.sh b/run_replay_gecode.sh index d7c2fe4..8f320ba 100755 --- a/run_replay_gecode.sh +++ b/run_replay_gecode.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env zsh +#!/usr/bin/env bash trap "exit" INT set -e diff --git a/run_restart_chuffed.sh b/run_restart_chuffed.sh index cf80e9c..718bb1b 100755 --- a/run_restart_chuffed.sh +++ b/run_restart_chuffed.sh @@ -1,4 +1,4 @@ -#!/bin/zsh +#!/usr/bin/env bash trap "exit" INT set -e diff --git a/run_restart_gecode.sh b/run_restart_gecode.sh index 2ed3106..4ef5053 100755 --- a/run_restart_gecode.sh +++ b/run_restart_gecode.sh @@ -1,4 +1,4 @@ -#!/bin/zsh +#!/usr/bin/env bash trap "exit" INT set -e diff --git a/setup.sh b/setup.sh index 2564e3f..eb79468 100644 --- a/setup.sh +++ b/setup.sh @@ -1,4 +1,4 @@ -#!/usr/bin/env zsh +#!/usr/bin/env bash timeout_sec=120 record_timeout_sec=240