Closed bertsky closed 1 year ago
- add kill button (dummy for now)
@SvenMarcus to implement this, we would need to "log in" to the Manager and kill the given process ID. But I don't like the Monitor to hold the keys. Perhaps we should instead start implementing our minimalistic web server in the Manager itself – delegating to for_production.sh
, for_presentation.sh
(which we will need for new jobs anyway) and to the killer.
Sry, I'll update the CI tests shortly.
All right thanks. When the pytest
problem is solved I give my approve.
process_id
must be a str not an int, esp. for process_mets.sh$REMOTEDIR/ocrd.pid
(on Controller), not from$PID
(on Manager)