devtools/devctl.py
branchstable
changeset 8451 49e965bba1ec
parent 8257 d54fc706d623
child 8454 113184eb4e06
--- a/devtools/devctl.py	Fri Jul 06 08:59:28 2012 +0200
+++ b/devtools/devctl.py	Fri Jul 06 09:01:42 2012 +0200
@@ -726,7 +726,7 @@
     min_args = max_args = 1
     options = [
         ('output-file',
-         {'type':'file', 'default': None,
+         {'type':'string', 'default': None,
           'metavar': '<file>', 'short':'o', 'help':'output image file',
           'input':False,
           }),