diff --git a/docs/devhelp/html2xml.py b/docs/devhelp/html2xml.py
index aa425a1fc2..b437eab8ef 100644
--- a/docs/devhelp/html2xml.py
+++ b/docs/devhelp/html2xml.py
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/python
import formatter
import htmllib
import os