diff options
| author | Maxime Dénès | 2016-10-21 10:02:38 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-21 10:02:38 +0200 |
| commit | 48546f7afa6ded3dc84109ac4f50c6fd193f2165 (patch) | |
| tree | 687b1f672c495785b13aa32948fb1c0aa1931c75 /kernel/cemitcodes.ml | |
| parent | 6d5fe92efbe3f6269666644a0f2e8e9aab8ab307 (diff) | |
| parent | e6f6cff7b88a70fe694507efe12885a776ab6730 (diff) | |
Merge remote-tracking branch 'github/pr/328' into v8.5
Was PR#328: Change the order of arguments of fig2dev.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions