[gnunet] branch master updated: -forgot to add new header to dist

[gnunet]

This is an automated email from the git hooks/post-receive script.

martin-schanzenbach pushed a commit to branch master
in repository gnunet.

The following commit(s) were added to refs/heads/master by this push:
     new 207304453 -forgot to add new header to dist
207304453 is described below

commit 207304453338746d16ef43b734010c30aacee412
Author: Martin Schanzenbach <schanzen@gnunet.org>
AuthorDate: Thu Dec 1 18:40:56 2022 +0900

    -forgot to add new header to dist
---
 src/include/Makefile.am | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/include/Makefile.am b/src/include/Makefile.am
index 15f5626ab..19450968c 100644
--- a/src/include/Makefile.am
+++ b/src/include/Makefile.am
@@ -10,7 +10,9 @@ EXTRA_DIST = \
   block_regex.h
 
 gnunetinclude_HEADERS = \
-  platform.h gettext.h \
+  platform.h \
+  gnunet_platform.h \
+  gettext.h \
   compat.h \
   gnunet_abd_service.h \
   gnunet_applications.h \

-- 
To stop receiving notification emails like this one, please contact
gnunet@gnunet.org.