diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-04 22:22:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-25 18:06:09 +0100 |
| commit | b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea (patch) | |
| tree | 9a898913c2ed9588d42d6e67c7b62e4dda7fdf63 /kernel/uGraph.ml | |
| parent | 3940441dffdfc3a8f968760c249f6a2e8a1e0912 (diff) | |
Fix for case-insensitive path looking continued (#2554): Adding a
second chance to dynamically regenerate the file system cache when a
file is not found (suggested by Guillaume M.).
Diffstat (limited to 'kernel/uGraph.ml')
0 files changed, 0 insertions, 0 deletions