devtools/devctl.py
changeset 8454 113184eb4e06
parent 8258 88a7d2c49d39
parent 8451 49e965bba1ec
child 8537 e30d0a7f0087
child 8857 5d08086c3e6d
--- a/devtools/devctl.py	Fri Jul 06 09:00:33 2012 +0200
+++ b/devtools/devctl.py	Fri Jul 06 14:31:13 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,
           }),