-
Nicolas George authored
It is no longer used anywhere. Furthermore, the header it was declared in was not installed, so it can not be considered part of the public API.
317b2b7e
It is no longer used anywhere. Furthermore, the header it was declared in was not installed, so it can not be considered part of the public API.