# HG changeset patch
# User blanchet
# Date 1283162997 -7200
# Node ID a243f8883e8e5eca593670a71eb76b80ba400e30
# Parent  92ca38d18af039702da8ebdb66df81d5841599cf
execute actions in same order as specified on command line

diff -r 92ca38d18af0 -r a243f8883e8e src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 30 12:02:51 2010 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 30 12:09:57 2010 +0200
@@ -75,7 +75,7 @@
 
 END
 
-foreach (split(/:/, $actions)) {
+foreach (reverse(split(/:/, $actions))) {
   if (m/([^[]*)(?:\[(.*)\])?/) {
     my ($name, $settings_str) = ($1, $2 || "");
     $name =~ s/^([a-z])/\U$1/;