diff options
Diffstat (limited to 'Build/source/texk/web2c/mf.ch')
-rw-r--r-- | Build/source/texk/web2c/mf.ch | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/Build/source/texk/web2c/mf.ch b/Build/source/texk/web2c/mf.ch index bfd297440e8..411ec092ccd 100644 --- a/Build/source/texk/web2c/mf.ch +++ b/Build/source/texk/web2c/mf.ch @@ -646,12 +646,14 @@ procedure jump_out; begin goto end_of_MF; end; @y -@ The |jump_out| procedure just cuts across all active procedure levels and -simply calls +@ The |jump_out| procedure just cuts across all active procedure levels. +The body of |jump_out| simply calls `|close_files_and_terminate|;\thinspace' followed by a call on some system procedure that quietly terminates the program. @^system dependencies@> +@f noreturn==procedure + @d do_final_end==begin update_terminal; ready_already:=0; |