[gnunet] 01/03: build: delete deprecated buildfiles for docs

[gnunet]

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

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

commit 8e77eaf45bc05a28baf0f009fa3b21660dbb0bfb
Author: Martin Schanzenbach <schanzen@gnunet.org>
AuthorDate: Mon Oct 16 13:24:01 2023 +0200

    build: delete deprecated buildfiles for docs
---
 contrib/gnunet_infrastructure/handbook_pull.sh | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/contrib/gnunet_infrastructure/handbook_pull.sh 
b/contrib/gnunet_infrastructure/handbook_pull.sh
deleted file mode 100755
index 16c7430ae..000000000
--- a/contrib/gnunet_infrastructure/handbook_pull.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-#!/bin/sh
-#
-# This essentially could be solved by:
-# git config pull.rebase true
-# git config rebase.autoStash true
-# but chances are that this is easy to
-# forget.
-# so execute this file on the server
-# instead of setting a git config.
-
-echo "Running git pull with autoStash and rebase"
-echo "If anything breaks in the future, delete"
-echo "and repeat - it was once considered to"
-echo "be responsible for non-trivial conflicts!"
-echo "We apply this because we need to build the"
-echo "handbook and tutorial without manual interventions."
-
-git pull --rebase --autostash

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