diff options
| author | Maxime Dénès | 2017-11-03 10:46:00 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-03 10:46:00 +0100 |
| commit | cc91f5703fa9f51fb0470e6c0d784c8a976fb452 (patch) | |
| tree | 7c5948d3351a82ed4905b436b1d0830866ba08a4 /kernel/nativecode.ml | |
| parent | 97bd47dbd61ca0b8f8a004fdec99f26dc7b032db (diff) | |
| parent | 105797d2b800c1bde1e0e614d258be7fb2e0f444 (diff) | |
Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions