38122544ed
The previous code converted option values to ints when the value contained a digit somewhere. This is too eager since it also converts strings like `release-0.2` to an int which should not happen. We now only convert to int when the value is an integer.