/* Dummy CSS file, used by browser_cache.js. */