vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

export index.production.min.js

Open onriv opened this issue 6 months ago • 0 comments

checking https://www.npmjs.com/package/@leanprover/infoview?activeTab=code, export index.production.min.js rather than export index.development.js for only index.production.min.js in the dist

onriv avatar Aug 15 '24 16:08 onriv