Drop platform: advice to shutdown workers#39

Merged

hannesm merged 3 commits intorobur-coop:mainfrom reynir:drop-platform-help

Dec 4, 2023

+143-41

Commits on Nov 20, 2023

Drop platform: advice to shutdown workers
reynir
committed

Commits on Nov 21, 2023

Persist dropped platforms, undrop command
reynir
committed

Commits on Dec 4, 2023

add undrop_platform command to client; transport dropped_platforms in info command
robur-team
committed