From 682407f2d5048cf034faf75b3e3611db31850f91 Mon Sep 17 00:00:00 2001
From: gcmalloc <gcmalloc@gmail.com>
Date: Fri, 7 Dec 2012 21:40:06 +0100
Subject: [PATCH] little correction on the readme

---
 devscripts/make_readme.py | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/devscripts/make_readme.py b/devscripts/make_readme.py
index 57ff0456e..7f2ea319c 100644
--- a/devscripts/make_readme.py
+++ b/devscripts/make_readme.py
@@ -1,11 +1,11 @@
 import sys
 import re
 
+README_FILE = 'README.md'
 helptext = sys.stdin.read()
 
-f = open('README.md')
-oldreadme = f.read()
-f.close()
+with open(README_FILE) as f:
+    oldreadme = f.read()
 
 header = oldreadme[:oldreadme.index('# OPTIONS')]
 footer = oldreadme[oldreadme.index('# CONFIGURATION'):]
@@ -14,8 +14,7 @@ options = helptext[helptext.index('  General Options:')+19:]
 options = re.sub(r'^  (\w.+)$', r'## \1', options, flags=re.M)
 options = '# OPTIONS\n' + options + '\n'
 
-f = open('README.md', 'w')
-f.write(header)
-f.write(options)
-f.write(footer)
-f.close()
\ No newline at end of file
+with open(README_FILE, 'w') as f:
+    f.write(header)
+    f.write(options)
+    f.write(footer)
-- 
2.22.2