aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.github/isabelle-action/Dockerfile1
-rw-r--r--.github/workflows/ci.yml1
2 files changed, 2 insertions, 0 deletions
diff --git a/.github/isabelle-action/Dockerfile b/.github/isabelle-action/Dockerfile
index 2c7af73..34a4adf 100644
--- a/.github/isabelle-action/Dockerfile
+++ b/.github/isabelle-action/Dockerfile
@@ -23,3 +23,4 @@ COPY entrypoint.sh /entrypoint.sh
RUN chmod +x /entrypoint.sh
ENTRYPOINT ["/entrypoint.sh"]
+
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 36b01ec..415afd1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -4,6 +4,7 @@ on: push
jobs:
build:
name: build ROOT
+ description: "Build repository ROOT file"
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v1