Remove the deprecated "log-timing" RPC log option#4573

rv-jenkins merged 1 commit intodevelopruntimeverification/k:developfrom

georgy/remove-deprecated-log-optionsruntimeverification/k:georgy/remove-deprecated-log-optionsCopy head branch name to clipboard