diff options
| author | Maxime Dénès | 2017-11-24 15:47:20 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-24 15:47:20 +0100 |
| commit | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (patch) | |
| tree | 580d80983daa71846662276080cc9fa9e789681f /kernel/term.mli | |
| parent | b8673b96bd7bbc40e442d308e6a30db4e699b2b1 (diff) | |
| parent | 1dfa6c551d95a82c242a514b81dd8cfac6f478d3 (diff) | |
Merge PR #6231: Fix link to Recursive Make Considered Harmful
Diffstat (limited to 'kernel/term.mli')
0 files changed, 0 insertions, 0 deletions