diff options
author | Christian Grothoff <christian@grothoff.org> | 2020-12-28 23:47:01 +0100 |
---|---|---|
committer | Christian Grothoff <christian@grothoff.org> | 2020-12-28 23:47:01 +0100 |
commit | 38b2445cbe48df349438c50670cf194544897de6 (patch) | |
tree | a54fcfe21efecb31a5f6cb2ddfea8a217b594c70 /doc | |
parent | e30fd985fd765ad25505c3d73d35e8535512ed2e (diff) | |
download | gnunet-38b2445cbe48df349438c50670cf194544897de6.tar.gz gnunet-38b2445cbe48df349438c50670cf194544897de6.zip |
fix some linting issues
Diffstat (limited to 'doc')
-rwxr-xr-x | doc/man/produce_html.sh.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/man/produce_html.sh.in b/doc/man/produce_html.sh.in index d2bd768a8..8680c0106 100755 --- a/doc/man/produce_html.sh.in +++ b/doc/man/produce_html.sh.in | |||
@@ -1,4 +1,4 @@ | |||
1 | #!/bin/sh | 1 | #!/bin/bash |
2 | 2 | ||
3 | if test -e @PKGDATADIRECTORY@/existence.sh | 3 | if test -e @PKGDATADIRECTORY@/existence.sh |
4 | then | 4 | then |