mathlib3
fix(dev-scripts): restore ctrl-c protection
#898
Merged

fix(dev-scripts): restore ctrl-c protection #898

mergify merged 2 commits into master from signal
kim-em
trying to work out what was wrong with catching signals
4eb9c2e1
kim-em kim-em requested a review from cipher1024 cipher1024 7 years ago
kim-em kim-em requested a review 7 years ago
kim-em kim-em changed the title fix(dev-scripts) fix(dev-scripts): restore ctrl-c protection 7 years ago
cipher1024
cipher1024 approved these changes on 2019-04-08
cipher1024 cipher1024 added ready-to-merge
Merge branch 'master' into 'signal'
00a40fb0
mergify mergify merged 5d81ab17 into master 7 years ago
mergify mergify deleted the signal branch 7 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone