diff options
| author | Maxime Dénès | 2017-05-03 18:58:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-03 18:58:21 +0200 |
| commit | 398e64567386656f8c20b75cccff6ea4805dbd79 (patch) | |
| tree | 00b0a1fb7cf66d4bf6fd096e23fc177ed38a7b95 /dev/ci | |
| parent | 510701319b1b0420698e411e24022a0fbec7c36c (diff) | |
| parent | 4a84961049f4f00897ae72a13954edbcc9aaba5e (diff) | |
Merge PR#603: Fix outdated description in RefMan.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions