remove unnecessary line in `scripts/update_mathlib.sh` · fpvandoorn/BonnAnalysis@6f3fb43

Triggered via push November 8, 2024 16:31

master

Status Success

Total duration 40m 36s

Artifacts 1

push.yml

on: push

Produced during runtime

Name	Size
github-pages Expired	34.2 MB