[build] Resurrect ide-project and collab addon
Showing
- .gitignore 1 addition, 0 deletions.gitignore
- Makefile 10 additions, 8 deletionsMakefile
- dune 12 additions, 0 deletionsdune
- frontend/classic/js/addon/public-path.js 1 addition, 1 deletionfrontend/classic/js/addon/public-path.js
- frontend/classic/js/coq-manager.js 2 additions, 2 deletionsfrontend/classic/js/coq-manager.js
- webpack.config.js 66 additions, 70 deletionswebpack.config.js
Please register or sign in to comment