def tip.strip

ezx@1.11.0.0 · src/git/git.bend:202

import ezx@1.11.0.0/src/git/git.bend as Git
import 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)), "")

Uses (5)

Used by (1)