From ad569761319fe71253ed8d51daacdd77df0b97cb Mon Sep 17 00:00:00 2001
From: Christian Helmuth <christian.helmuth@genode-labs.com>
Date: Mon, 26 Feb 2018 17:05:34 +0100
Subject: [PATCH] tool/publish: fix help for PUBLIC_DIR

---
 tool/depot/publish | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tool/depot/publish b/tool/depot/publish
index b638b9fa2..1357a7902 100755
--- a/tool/depot/publish
+++ b/tool/depot/publish
@@ -12,7 +12,7 @@ define HELP_MESSAGE
 
   usage:
 
-    $(firstword $(MAKEFILE_LIST)) <archive-path> {PUBLIC=<public>}
+    $(firstword $(MAKEFILE_LIST)) <archive-path> {PUBLIC_DIR=<public>}
 
   The <archive-path> denotes the archives (and implicitly their
   dependencies) to publish from the depot to the public directory.
@@ -21,7 +21,7 @@ define HELP_MESSAGE
   This tool does not touch any Genode source repository. It solely
   reads from the depot and writes to the public directory.
 
-  The optional 'PUBLIC' argument defines the location of the public
+  The optional 'PUBLIC_DIR' argument defines the location of the public
   directory. If not specified, '<genode-dir>/public/' is used.
 
 endef