diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-02-20 19:08:10 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-02-24 15:07:34 -0500 |
| commit | e156a0703b700d7d0cf18fbf5d9d39a83e8a6e5c (patch) | |
| tree | 7c3d096472b2bf86755c7db6d7a8bc38ebbc2de4 /plugins/ltac/pltac.ml | |
| parent | 70f1d999ff030d20d10f23bcbf95f37216e182c9 (diff) | |
[test-suite] Move sed scripts into bash arrays
Diffstat (limited to 'plugins/ltac/pltac.ml')
0 files changed, 0 insertions, 0 deletions