Fix previous commit missing the header file

Pierre Bürkirequested to merge
hotfix into develop

Glorious one-line, one-commit merge request

Merge request reports