From baf70ef93db68eed049753dc8136c7b3dd6b78a8 Mon Sep 17 00:00:00 2001
From: Stefan van der Walt <stefan@sun.ac.za>
Date: Sat, 19 Oct 2013 16:43:59 +0200
Subject: [PATCH] Correctly determine dev version for doc building.

---
 doc/gh-pages.py | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/doc/gh-pages.py b/doc/gh-pages.py
index af992158..8fe4ee01 100644
--- a/doc/gh-pages.py
+++ b/doc/gh-pages.py
@@ -86,13 +86,14 @@ if __name__ == '__main__':
         if l.startswith('VERSION'):
             tag = l.split("'")[1]
 
-            # Rename to, e.g., 0.9.x
-            tag = '.'.join(tag.split('.')[:-1] + ['x'])
+            if "dev" in tag:
+                tag = "dev"
+            else:
+                # Rename e.g. 0.9.0 to 0.9.x
+                tag = '.'.join(tag.split('.')[:-1] + ['x'])
 
             break
 
-    if "dev" in tag:
-        tag = "dev"
 
     startdir = os.getcwd()
     if not os.path.exists(pages_dir):