This file is in the public domain.  */


 * This file is in the public domain.


# This file is in the public domain.


See also
<https://www.gnu.org/prep/maintain/html_node/License-Notices-for-Other-Files.html>
and <https://www.gnu.org/licenses/license-list.en.html#PublicDomain>.