diff options
| author | Maxime Dénès | 2016-12-02 12:54:56 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-12-02 12:54:56 +0100 |
| commit | cf98b736a15b8d1e69a0a04c192e77cf69eb01db (patch) | |
| tree | 25de28f1fa30c5147fcd927bc2c650cd9cc4f739 /kernel/names.ml | |
| parent | e048e4d5505cf73ae92016c5175932e15863f95e (diff) | |
| parent | 1099b748bb080d449037fbd06199c012fa3ce387 (diff) | |
Merge remote-tracking branch 'github/pr/380' into v8.6
Was PR#380: Fix bug #5232: proper globalization of hints paths
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions