Use non-deprecated header

Authored by vkrause on Nov 12 2019, 7:37 PM.

Description

Use non-deprecated header

Details

Committed
vkrauseNov 12 2019, 7:37 PM
Parents
R91:e1357ae39eba: GIT_SILENT: Prepare 5.13.0beta1
Branches
Unknown
Tags
Unknown
References
tag: v19.11.80