Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix missing pipe in check_ci (#1926)
Bugfix: left out pipe to word count` | wc -l` after updating: `num_platforms=$(ls ../platforms/config.* | wc -l)` to `num_platforms=$(find ../platforms -type f -name "config.*")` when it was flagged by the BASH linter.
- Loading branch information