chore: Remmove check_file_import.yml
This commit is contained in:
parent
524fccc484
commit
a8babe70f7
1 changed files with 0 additions and 23 deletions
23
.github/workflows/check_file_import.yml
vendored
23
.github/workflows/check_file_import.yml
vendored
|
@ -1,23 +0,0 @@
|
|||
on:
|
||||
push:
|
||||
pull_request:
|
||||
|
||||
name: check file import
|
||||
|
||||
jobs:
|
||||
check_file_import:
|
||||
name: check file import
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: clean up
|
||||
run: |
|
||||
find . -name . -o -prune -exec rm -rf -- {} +
|
||||
|
||||
- uses: actions/checkout@v4
|
||||
|
||||
- name: update HepLean.lean
|
||||
run: |
|
||||
git ls-files 'HepLean/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > HepLean.lean
|
||||
|
||||
- name: check that all files are imported
|
||||
run: git diff --exit-code
|
Loading…
Add table
Add a link
Reference in a new issue