chore: tiny typo in lake globs syntax#717

alexb-harmonic wants to merge 1 commit intoleanprover:mainleanprover/reference-manual:mainfrom

alexb-harmonic:patch-1alexb-harmonic/reference-manual:patch-1Copy head branch name to clipboard