aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xjobs/acl2-theorems.before4
l---------[-rwxr-xr-x]jobs/acl2-theorems.develop.before7
2 files changed, 5 insertions, 6 deletions
diff --git a/jobs/acl2-theorems.before b/jobs/acl2-theorems.before
index de7c2c9..f21a912 100755
--- a/jobs/acl2-theorems.before
+++ b/jobs/acl2-theorems.before
@@ -2,5 +2,9 @@
set -euo pipefail
git clone https://git.tojo.tokyo/acl2-theorems.git .
+echo
+git checkout "${branch:-master}"
+echo '---'
git log -n 1
+echo '---'
echo
diff --git a/jobs/acl2-theorems.develop.before b/jobs/acl2-theorems.develop.before
index 088f78a..05c494d 100755..120000
--- a/jobs/acl2-theorems.develop.before
+++ b/jobs/acl2-theorems.develop.before
@@ -1,6 +1 @@
-#!/usr/bin/env bash
-set -euo pipefail
-
-git clone https://git.tojo.tokyo/acl2-theorems.git .
-git checkout "$branch"
-git log -n 1
+./acl2-theorems.before \ No newline at end of file