Clarify role of generate-documentation.py

diff --git a/generate-documentation.py b/generate-documentation.py
index 056de06..2f91503 100755 (executable)
--- a/generate-documentation.py
+++ b/generate-documentation.py
@@ -1,4 +1,7 @@
 #!/usr/bin/python
+
+# Generate docs/options.html
+
 import json
 import glob
 import re