+/* Exit orderly, clean up in an order respecting resource dependencies. */
+extern void exit_game();
+
+/* If "err" == 0, do nothing. Else, clean up and exit with an error message that
+ * consists, first, of "msg" or (if "msg" is a NULL pointer) a generic "Details
+ * unknown", secondly of "err" as the "internal error code", and thirdly of
+ * errno if it is non-zero.