Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix build for Ubuntu 16.04 where the compilation failed because of some unused parameters. To fix this I marked the unused a parameters in DummySearch the same way it is done in other parts of the code.
- Loading branch information