diff options
| author | spanjel | 2019-08-08 02:12:31 -0700 |
|---|---|---|
| committer | GitHub | 2019-08-08 02:12:31 -0700 |
| commit | 86e8deed878251e74534393a7b37a1471f7fa079 (patch) | |
| tree | 00920dcfe449a3d0661b6ac139aed3162daf4e15 /dev/ci/docker/bionic_coq | |
| parent | cce00f7a3f0c5fe101b713f32ca4c67ff5970121 (diff) | |
map directory read error to empty directory
Diffstat (limited to 'dev/ci/docker/bionic_coq')
0 files changed, 0 insertions, 0 deletions