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, }),