# HG changeset patch
# User wenzelm
# Date 1459705649 -7200
# Node ID 3fee575c9dce7f31068a94209fa1f2f2e2e52b9f
# Parent  eb94e570c1a45d43a2d691631d70b4137c918f5f
clarified usage;

diff -r eb94e570c1a4 -r 3fee575c9dce lib/Tools/getenv
--- a/lib/Tools/getenv	Sat Apr 02 23:29:05 2016 +0200
+++ b/lib/Tools/getenv	Sun Apr 03 19:47:29 2016 +0200
@@ -57,6 +57,7 @@
 
 # args
 
+[ -z "$ALL" -a -z "$DUMP" -a "$#" -eq 0 ] && usage
 [ -n "$ALL" -a "$#" -ne 0 ] && usage