diff options
| author | Emilio Jesus Gallego Arias | 2018-10-31 13:56:28 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-31 13:56:28 +0100 |
| commit | 5c951efbc27e6061f80b839d7a1c862d8fb4c587 (patch) | |
| tree | 6a509a32cf0850aa3a843209b6dfebe66f46cce7 /kernel/nativecode.mli | |
| parent | ec73ad521123e11ad8e1c6c916de48ae30b12639 (diff) | |
| parent | 2a38552ad35cdcd827da014106aa5b4af88dfb9e (diff) | |
Merge PR #8867: Notations: fixing a bug when printing abbreviations in custom entries.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions