# HG changeset patch # User wenzelm # Date 1624896606 -7200 # Node ID d7ac039421ece0853bab6c25a0b8f9f4a79b73b8 # Parent eb7655fcb090a6554b14d0df000de1da7c7a3667 proper usage; diff -r eb7655fcb090 -r d7ac039421ec src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Mon Jun 28 14:43:33 2021 +0200 +++ b/src/Pure/Admin/build_release.scala Mon Jun 28 18:10:06 2021 +0200 @@ -861,7 +861,7 @@ var rev = "" val getopts = Getopts(""" -Usage: Admin/build_release [OPTIONS] BASE_DIR +Usage: Admin/build_release [OPTIONS] Options are: -A REV corresponding AFP changeset id