def tip.strip
import ezx@1.11.0.0/src/git/git.bend as Gitimport Base
202# the prefix taken off when it is there, and "" when it is not, so a commit
203# line is not mistaken for a branch name
204def tip.strip(+text: String, +pre: String) -> String:
205 Bool.pick(String, String.starts_with(text, pre),
206 String.drop(text, String.length(pre)), "")