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)) {PUBLIC=} + $(firstword $(MAKEFILE_LIST)) {PUBLIC_DIR=} The 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, '/public/' is used. endef