ehmry/genode
ehmry
/
genode
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

tool/publish: fix help for PUBLIC_DIR

This commit is contained in:
Christian Helmuth 2018-02-26 17:05:34 +01:00
parent 77c5e55f4f
commit ad56976131
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
tool/depot/publish
View File

@ -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