diff options
author | w0rp <w0rp@users.noreply.github.com> | 2019-06-10 13:33:54 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-10 13:33:54 +0100 |
commit | 730752523b31167909a2c895b35eb1051cbfbb39 (patch) | |
tree | f7d9ab42222ffa425a00ece25b198e5bb19c5591 /test/handler/test_idris_handler.vader | |
parent | d9bad6c0b83b51da1c8e83f5b72e58e8755453c8 (diff) | |
parent | b41eecd31bb7fe56de838d15fc632f51856a80cb (diff) | |
download | ale-730752523b31167909a2c895b35eb1051cbfbb39.zip |
Merge pull request #2574 from enterprisey/patch-1
In README, more efficient git clones
Diffstat (limited to 'test/handler/test_idris_handler.vader')
0 files changed, 0 insertions, 0 deletions