diff options
| author | Hendrik Tews | 2016-12-15 09:39:00 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2016-12-15 09:39:00 +0100 |
| commit | b0553954a4324efd873f7caae85f0ebc0665883c (patch) | |
| tree | a9e66d5de552d516740270928930fc6aee6ccf32 /isar/Example.thy | |
| parent | 93a0d1ca16fd30e89e312932008106bc5503386f (diff) | |
die gracefully when visiting files in nonexisting directories
Diffstat (limited to 'isar/Example.thy')
0 files changed, 0 insertions, 0 deletions