Short name: “tex”.

If $(patch_tex_copy) already exists, check that content of $(patch_tex) is the same. If not, print the warning $(patch_reminder_message).

If $(patch_file) doesn't exist:

• copy $(patch_tex_orig) to $(patch_tex) and $(patch_tex_copy),

If $(patch_file) exists:

• apply the patch $(patch_file) to $(patch_tex_orig) and save the result as $(patch_tex).

• If error, create the file $(patch_error) and execute the step “Patch Work, Problems”.

• If success,

  • copy $(patch_tex) to $(patch_tex_copy), and

  • delete the files $(patch_error) and $(patch_error_rej).