[1541] Comment about pruning remote origin added.

diff --git a/tools/git-obsolete-branch.py b/tools/git-obsolete-branch.py
index 5abd4803f16ae96bdf71341bf3086a32644c9bf6..68ca51e95df87beace70ff0c3338ecd13fc7600a 100755 (executable)
--- a/tools/git-obsolete-branch.py
+++ b/tools/git-obsolete-branch.py
@@ -17,6 +17,11 @@
 #
 # This script lists obsolete (fully merged) branches. It is useful for periodic maintenance
 # of our GIT tree.
+
+# It is good to use following command before running this script:
+#
+# git pull
+# git remote prune origin
 #
 # This script requires python 2.7 or 3.
 #