diff options
| author | Gaëtan Gilbert | 2019-05-08 10:11:19 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-08 10:11:19 +0200 |
| commit | 3786fe758d6f3082b425070f961b805993bffaf4 (patch) | |
| tree | ac4aa8969fdb4277880b1a29c5c05e0c1ce4c2a5 /kernel/nativecode.ml | |
| parent | e30d52a3c724a71bf43b46416c09e4b6ef1d1f67 (diff) | |
| parent | 21e5a5d510de59a33f3e6a0f88b8321ac0d7d23d (diff) | |
Merge PR #10119: Show diffs in error messages only if Diffs is enabled
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions