script: Fix a bug when time_limit is not a number
Description
Description
Details
Details
- Committed
ncoudene Oct 17 2022, 14:47 - Pushed
ncoudene Oct 17 2022, 14:47 - Parents
- R11410:985f271ee9ad: Pylint warning/errors
- Branches
- Unknown
- Tags
script: Fix a bug when time_limit is not a number
script: Fix a bug when time_limit is not a number
Authored by ncoudene on Oct 17 2022, 14:47.
Tags
None
Subscribers
None