diff -r 5d3ec1198a64 -r f9682fdfd47b src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py	Thu Sep 12 10:35:33 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py	Thu Sep 12 10:40:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/usr/bin/python
+#!/usr/bin/env python
 #     Title:      HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
 #     Author:     Daniel Kuehlwein, ICIS, Radboud University Nijmegen
 #     Copyright   2012