diff options
| author | Christian Grothoff <christian@grothoff.org> | 2017-10-06 21:41:41 +0200 |
|---|---|---|
| committer | Christian Grothoff <christian@grothoff.org> | 2017-10-06 21:41:41 +0200 |
| commit | 98b7444a7b122498e5b6d693c4503b1702763307 (patch) | |
| tree | 2dfdac7f2a89a8ee8b10cf1cd2474dfa62516938 /.gitignore | |
| parent | 9b585fd066c238485b161b7664901e9d23ecf56b (diff) | |
handle hypothetical failure of plugin not found
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions