mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
mkdist.sh
script cleanup
Since Travis CI is no longer used.
This commit is contained in:
parent
ef91cc01c7
commit
bd94b91615
@ -20,7 +20,6 @@ git checkout tags/v"$1"
|
||||
rm -rf .git
|
||||
rm -rf .github
|
||||
rm .git*
|
||||
rm -f .travis*
|
||||
rm -rf Release
|
||||
rm -rf benchmark
|
||||
find . -type f -name '.gitignore' -exec rm -f {} \;
|
||||
|
Loading…
Reference in New Issue
Block a user