diff --git a/collects/meta/props b/collects/meta/props index bf1f0591c7..20b8af3d86 100755 --- a/collects/meta/props +++ b/collects/meta/props @@ -320,8 +320,13 @@ properties, intended to be used by meta tools: "known properties. The given paths are normalized to be relative to the" "plt root for the tree holding this script *if* it is in such a tree" "(determined by inspecting a few known directories), otherwise an error" - "is raised. Note that this script does not depend on the plt" - "installation that runs it, and that it holds the data that it changes." + "is raised. Note that this script holds the data that it changes, so you" + "need to commit it after changes are made. Also note that it does not" + "depend on the plt installation that runs it -- you just need to use the" + "script from the work directory that you want to deal with; if you add" + " prop = \"!$(git rev-parse --show-toplevel)/collects/meta/props\"" + "to your global git config file (usually ~/.gitconfig), then you'll be" + "able to run it as `git prop'." "" "Path arguments can also be given via stdin (each on a line) if the" "command-line path argument is a single `-'. In this mode the paths are"