# HG changeset patch
# User sultana
# Date 1334443937 -3600
# Node ID d2392e6cba7ff8995bfbd6c9a9c23d1065723ee0
# Parent  3fabf352243e5dce675479f2b77746fb74fa8f87
switched from using sed to perl in mirabelle tool

diff -r 3fabf352243e -r d2392e6cba7f 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
@@ -11,7 +11,7 @@
   ACTIONS="$MIRABELLE_HOME/Actions/mirabelle_*.ML"
   for ACTION in $ACTIONS
   do
-    echo $ACTION | sed 's/.*mirabelle_\(.*\)\.ML/    \1/'
+    echo $ACTION | perl -w -p -e 's/.*mirabelle_(.*)\.ML/    $1/'
   done
 }