diff options
| author | Jason Gross | 2018-02-20 19:08:10 -0500 |
|---|---|---|
| committer | Jason Gross | 2018-02-24 15:07:34 -0500 |
| commit | e156a0703b700d7d0cf18fbf5d9d39a83e8a6e5c (patch) | |
| tree | 7c3d096472b2bf86755c7db6d7a8bc38ebbc2de4 /dev | |
| parent | 70f1d999ff030d20d10f23bcbf95f37216e182c9 (diff) | |
[test-suite] Move sed scripts into bash arrays
As per https://github.com/coq/coq/pull/6756/files#r168028764
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions