mathlib3
fix(scripts/remote-install-update-mathlib): apt shouldn't ask
#969

Merged

fix(scripts/remote-install-update-mathlib): apt shouldn't ask #969

mergify merged 1 commit into master from remote-install-again

fix(scripts/remote-install-update-mathlib): apt shouldn't ask

1a81b7af

PatrickMassot requested a review 7 years ago

cipher1024 approved these changes on 2019-05-02

cipher1024 added ready-to-merge

mergify merged 60b3c198 into master 7 years ago

mergify deleted the remote-install-again branch 7 years ago

Reviewers

cipher1024

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone