Skip to content
Snippets Groups Projects
Commit de22c9ea authored by Shachar Itzhaky's avatar Shachar Itzhaky
Browse files

[bugfix] [build] Modules in global package.

Strictly speaking, is not good practice; but should be available for
quick-and-dirty experimentation.
parent 8cc872b2
Branches
No related tags found
No related merge requests found
......@@ -609,6 +609,7 @@ class JsCoqCompat {
var d: {[dp: string]: string[]} = {}
for (let k in manifest.modules) {
var [dp, mod] = k.split(/[.]([^.]+)$/);
if (!mod) { mod = dp; dp = ""; }
(d[dp] = d[dp] || []).push(mod);
}
var pkgs = Object.entries(d).map(([a,b]) => ({
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment