diff options
| author | Guillaume Melquiond | 2015-02-10 14:09:25 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-02-10 14:09:25 +0100 |
| commit | 48f58750125706b78b00284a541012982af4a17d (patch) | |
| tree | c8c31bfde89a1043258dbaf7bf696df55080610f /kernel/nativelambda.mli | |
| parent | 85458847345fdad2236da0171f6f0860992a9493 (diff) | |
Prevent Latex from messing with backticks. (Fix for bug #3871)
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions