Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CI: Drop obsolete, unused Travis CI configuration
5145d11 replaced Travis CI with GitHub Actions but forgot to delete this file.
- Loading branch information