# HG changeset patch
# User sultana
# Date 1334443937 -3600
# Node ID e6add51fd7ba85faf45e798841b297f02e2c8359
# Parent  d2392e6cba7ff8995bfbd6c9a9c23d1065723ee0
Mirabelle now gives usage info when no arguments given

diff -r d2392e6cba7f -r e6add51fd7ba src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Sat Apr 14 23:52:17 2012 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Sat Apr 14 23:52:17 2012 +0100
@@ -67,6 +67,8 @@
 
 # options
 
+[ $# -eq 0 ] && usage
+
 while getopts "L:T:O:t:q?" OPT
 do
   case "$OPT" in