aboutsummaryrefslogtreecommitdiff
path: root/.github/isabelle-action/entrypoint.sh
diff options
context:
space:
mode:
Diffstat (limited to '.github/isabelle-action/entrypoint.sh')
-rw-r--r--.github/isabelle-action/entrypoint.sh5
1 files changed, 5 insertions, 0 deletions
diff --git a/.github/isabelle-action/entrypoint.sh b/.github/isabelle-action/entrypoint.sh
new file mode 100644
index 0000000..954226a
--- /dev/null
+++ b/.github/isabelle-action/entrypoint.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+chmod +x /Isabelle/bin/isabelle
+sh -c "/Isabelle/bin/isabelle $INPUT_TOOL_ARGS"
+