Use another source map type in production

[timwis]

I changed it because of a new webpack bug (webpack/webpack#5931). But it turns out I changed it to a value that's not recommended for production (https://webpack.js.org/configuration/devtool/#devtool). Ideally the bug will get resolved, but we should change it to another value in the meantime. It's in webpack.config.js at the bottom.