diff options
| author | Emilio Jesus Gallego Arias | 2018-05-21 00:15:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-27 15:18:11 +0200 |
| commit | b34acd7904dac581b57f7282192a40f1afb870dc (patch) | |
| tree | bf55c06c3571047063abb652b9badd6e1a463cf3 /dev/ci | |
| parent | 311e87f261b5e7f1dca61ac19d9b7b695b411ce0 (diff) | |
[tactics] Turn boolean locality hint parameter into a named one.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions