diff options
| author | Maxime Dénès | 2017-12-11 09:25:55 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-11 09:25:55 +0100 |
| commit | b1b84b3a942375048db459d81d2b9bc7662f6ada (patch) | |
| tree | 97922688bb85f0585ed44700c4a6cbab39ec8016 /API/PROPERTIES | |
| parent | 84b41f2540440bbcb74aad1c8e93f7e0b9bc4b4e (diff) | |
| parent | 2434e85e1f2006e66efd74bd6cd7224e301e3bff (diff) | |
Merge PR #6351: Fix a copy-paste error in ci-ltac2.
Diffstat (limited to 'API/PROPERTIES')
0 files changed, 0 insertions, 0 deletions