(This was originally filed as #5182. Some immediate work has been done in #5196 -- thanks @vojtechjelinek! -- but there's still some more long term stuff to do, so I'm refiling.)

There is a limit of 10,000 on the number of files that can be uploaded to the production server. We have breached this limit enough times that it seems like it would be better to take active steps to control the number of files we deploy to production.

Here are some avenues for investigation:

• Remove jquery-ui-themes altogether from manifest.json -- it looks like we don't need it. (I think @vojtechjelinek is doing this?)
• Enforce that each dependency in manifest.json has a "bundle" option stating which of its files should be deployed to production. In general, each third-party library should not contribute more than one or two files to the release.
• Find a way to whitelist the subset of files in MathJax that are deployed (note that the MathJax library weighs in at 2k+ files, and some of these are loaded from the JS on-demand).
• We duplicate a bunch of files in build/ or backend_prod_files/, and we should not deploy those to production. We should create a reference doc explaining what we are doing in the build process so that we can exclude the unneeded files -- or, even better, find a way to organize things so that all the stuff we ignore / all the stuff we deploy automatically goes in a clearly-labelled folder.