mirror of
https://github.com/mmueller41/genode.git
synced 2026-01-21 20:42:56 +01:00
In the future bin_* means the direct destruction of a kernel object without any blocking. kill_* in contrast is used for bringing a kernel object such as signal contexts synchronized into a sleeping state from where they can be destructed without the risk of getting broken refs in userland. ref #989