diff --git a/src/history_manager.py b/src/history_manager.py old mode 100644 new mode 100755 index 7e5d9fbe6..1fedfb2cc --- a/src/history_manager.py +++ b/src/history_manager.py @@ -1,3 +1,4 @@ +#! /usr/bin/env python ## history_manager.py ## ## Copyright (C) 2006 Nikos Kouremenos