diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2016-05-18 07:34:24 +0200 |
|---|---|---|
| committer | Rémi Verschelde <remi@verschelde.fr> | 2016-05-18 07:34:24 +0200 |
| commit | 926495d8eb11de2878319ba54f30812fa1637d72 (patch) | |
| tree | 45512b79f16f1e2c32df785e3759a19fcc180412 /tools | |
| parent | 3e61927790ca64ee01a929b8cefa87bb052762c2 (diff) | |
| parent | ebcf04ff1fa37531f82b0c8d2a9f2df221d08198 (diff) | |
Merge pull request #4698 from volzhs/compile-no-tools
fix compile failure when tools=no
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions