diff options
| author |  jesopo | 2019-08-30 17:17:03 +0100 |
|---|---|---|
| committer | jesopo | 2019-08-30 17:17:03 +0100 |
| commit | e97e3c8f309c9e3260ceedbf961f80be8f8333ed (patch) | |
| tree | b1761571d3a0e92afa3315724d3b07eb21a780bb /modules/github.py | |
| parent | Add IntRangeSetting, reorder OptionsSetting arg order (diff) | |
| signature | ||
add utils.deadline(func, seconds) to put hard limits on code exec time
Diffstat (limited to 'modules/github.py')
0 files changed, 0 insertions, 0 deletions