diff --git a/tools/update_revnum.py b/tools/update_revnum.py index 9567c1f..7191114 100755 --- a/tools/update_revnum.py +++ b/tools/update_revnum.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python """ Change the revision number in Release.py """ import os