with Failure _ ->
command_error (sprintf "Not an integer value \"%s\"" value))
in
- { status with options = StringMap.add name value status.options }
+ if StringMap.mem name status.options && name = "baseuri" then
+ command_error "Redefinition of 'baseuri' is forbidden."
+ else
+ { status with options = StringMap.add name value status.options }
(* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
class type console =