# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1444393202 -7200
# Node ID e82caf5f5a8a4b887308e0b3272c81bc1ab4379f
# Parent  6890aa1afe3e83b330251ee3b9e4bbfbc2bfb54a
Fixed option handling at the end of the argument list.

diff -r 6890aa1afe3e -r e82caf5f5a8a optimiser.py
--- a/optimiser.py	Fri Oct 09 12:04:16 2015 +0200
+++ b/optimiser.py	Fri Oct 09 14:20:02 2015 +0200
@@ -277,7 +277,7 @@
 def get_float(options, flag):
     try:
         i = options.index(flag)
-        if options[i+1].isdigit():
+        if i+1 < len(options) and options[i+1].isdigit():
             return float(options[i+1])
         else:
             return 1.0