A file installed by a function called by do_install