I took Ed's advice and moved the plugin stuff to its own top-level directory. This is an attempt to solve the problem of copying files that we have experienced. In any case, it will serve as a place to stick additional plugins.