File tree Expand file tree Collapse file tree 2 files changed +34
-0
lines changed Expand file tree Collapse file tree 2 files changed +34
-0
lines changed Original file line number Diff line number Diff line change 1+ name : Basic checks
2+ on :
3+ pull_request :
4+ push :
5+ branches :
6+ - master
7+ jobs :
8+ basic-checks :
9+ runs-on : ubuntu-latest
10+ steps :
11+ - name : Checkout
12+ uses : actions/checkout@v4
13+ - name : Check consistency of files in Makefiles
14+ run : dev/tools/check-make-sync.sh
Original file line number Diff line number Diff line change 1+ #! /bin/sh
2+
3+ MAKE_FILES=$( find theories -name " Make.*" )
4+
5+ FILES_OTHERS=files_others__
6+ FILES_ALL=files_all__
7+
8+ rm -f ${FILES_OTHERS} ${FILES_ALL}
9+ grep " [.]v" ${MAKE_FILES} | sed -e ' s/.*://' | sort > ${FILES_OTHERS}
10+ find theories -name " *.v" | sed -e ' s_theories/__' | sort > ${FILES_ALL}
11+
12+ if $( diff -q ${FILES_OTHERS} ${FILES_ALL} > /dev/null) ; then
13+ echo " Make.* match files in theories/"
14+ else
15+ echo " Make.* and files in theories/ don't match"
16+ diff ${FILES_OTHERS} ${FILES_ALL}
17+ exit 1
18+ fi
19+
20+ rm -f ${FILES_OTHERS} ${FILES_ALL}
You can’t perform that action at this time.
0 commit comments