From c7f33d579aa3b05ac3e96800e05ddcea40e67c97 Mon Sep 17 00:00:00 2001 From: adomani Date: Fri, 17 May 2024 15:39:40 +0200 Subject: [PATCH] first custom action --- .github/workflows/mathlib_stats.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/mathlib_stats.yml b/.github/workflows/mathlib_stats.yml index 48eeaa17000d4..071bb34bd1bcb 100644 --- a/.github/workflows/mathlib_stats.yml +++ b/.github/workflows/mathlib_stats.yml @@ -11,11 +11,11 @@ jobs: steps: - name: Checkout master branch - uses: actions/checkout@v4 - with: - ## fetch the whole repository, to get the history of the last week - fetch-depth: 0 - ref: 'master' + uses: adomani/get_mathlib4_with_cache/tree/first_attempt@v1 #actions/checkout@v4 + #with: + # ## fetch the whole repository, to get the history of the last week + # fetch-depth: 0 + # ref: 'master' # - name: mathlib_stats - id: mathlib_stats