mathlib3
fix(dev-scripts): restore ctrl-c protection
#898
Merged
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Overview
Commits
2
Changes
View On
GitHub
fix(dev-scripts): restore ctrl-c protection
#898
mergify
merged 2 commits into
master
from
signal
trying to work out what was wrong with catching signals
4eb9c2e1
kim-em
requested a review
from
cipher1024
7 years ago
kim-em
requested a review
7 years ago
kim-em
changed the title
fix(dev-scripts)
fix(dev-scripts): restore ctrl-c protection
7 years ago
cipher1024
approved these changes on 2019-04-08
cipher1024
added
ready-to-merge
Merge branch 'master' into 'signal'
00a40fb0
mergify
merged
5d81ab17
into master
7 years ago
mergify
deleted the signal branch
7 years ago
Login to write a write a comment.
Login via GitHub
Reviewers
cipher1024
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub