diff -r 3ac2878764f9 -r 42e02ddd1568 lib/scripts/unsymbolize
--- a/lib/scripts/unsymbolize	Wed Jul 10 16:25:26 2013 +0200
+++ b/lib/scripts/unsymbolize	Fri Jul 12 14:28:19 2013 +0200
@@ -2,8 +2,7 @@
 #
 # Author: Markus Wenzel, TU Muenchen
 #
-# unsymbolize.pl - remove unreadable symbol names from sources
-#
+# unsymbolize - remove unreadable symbol names from sources
 
 use warnings;
 use strict;
@@ -46,7 +45,7 @@
     my $result = $_;
 
     if ($text ne $result) {
-        print STDERR "fixing $file\n";
+        print STDERR "changing $file\n";
         if (! -f "$file~~") {
             rename $file, "$file~~" || die $!;
         }