diff options
| author | Pierre-Marie Pédrot | 2018-03-09 10:27:39 -0300 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-03-09 10:27:39 -0300 |
| commit | d2d1fe30e3defa18dd966bf8160df81fc1e72e31 (patch) | |
| tree | 59eddd1ea50317bbc55f40d0df53aaa38dfec7a8 /dev | |
| parent | ba27c2e21f80b41dfd837e6c6b15f82ca405cf04 (diff) | |
Fix compilation after the change of API in options.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions