diff options
| author | Kevin Clark <kevin.clark@gmail.com> | 2020-11-27 20:32:51 -0800 |
|---|---|---|
| committer | Kevin Clark <kevin.clark@gmail.com> | 2020-11-27 20:32:51 -0800 |
| commit | f72e60c12a825f30cf25c585c7876fce1c99099d (patch) | |
| tree | 1ea040c12152ce94a6a8b1116eae0972ea45d7ba /doc/ale-idris.txt | |
| parent | 1365dce921c1fb84a668ae121d5d5aeebef99fbc (diff) | |
| download | ale-f72e60c12a825f30cf25c585c7876fce1c99099d.zip | |
Fix check-supported-tools-tables check
sed wasn't using -E, so '|' wasn't being handled properly. Seems likely
that's sed-implementation specific, so now it runs through docker's sed
to support portability.
Diffstat (limited to 'doc/ale-idris.txt')
0 files changed, 0 insertions, 0 deletions