Git.tip.strip: def of ezx@1.13.0.0
Import: import ezx@1.13.0.0/src/git/git.bend as Git
Lines 202-206 of ezx@1.13.0.0/src/git/git.bend: https://jend.leeeet.dev/read.txt?path=ezx@1.13.0.0/src/git/git.bend&start_line=202&end_line=206

import Base

# the prefix taken off when it is there, and "" when it is not, so a commit
# line is not mistaken for a branch name
def tip.strip(+text: String, +pre: String) -> String:
  Bool.pick(String, String.starts_with(text, pre),
    String.drop(text, String.length(pre)), "")

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.starts_with