Flatten directory structure.
parent
d4dd6b1ba7
commit
ed53c3f95e
|
@ -16,9 +16,9 @@
|
||||||
{"git":
|
{"git":
|
||||||
{"url": "https://github.com/jrpotter/bookshelf-docgen.git",
|
{"url": "https://github.com/jrpotter/bookshelf-docgen.git",
|
||||||
"subDir?": null,
|
"subDir?": null,
|
||||||
"rev": "ef54a19e670a19ee2a17a3bc70bfe4006b8e2a7a",
|
"rev": "b083d636c2581e72da9d18023240319dd5eca43a",
|
||||||
"name": "doc-gen4",
|
"name": "doc-gen4",
|
||||||
"inputRev?": "ef54a19e670a19ee2a17a3bc70bfe4006b8e2a7a"}},
|
"inputRev?": "b083d636c2581e72da9d18023240319dd5eca43a"}},
|
||||||
{"git":
|
{"git":
|
||||||
{"url": "https://github.com/mhuisi/lean4-cli",
|
{"url": "https://github.com/mhuisi/lean4-cli",
|
||||||
"subDir?": null,
|
"subDir?": null,
|
||||||
|
|
|
@ -12,7 +12,7 @@ require std4 from git
|
||||||
"6006307d2ceb8743fea7e00ba0036af8654d0347"
|
"6006307d2ceb8743fea7e00ba0036af8654d0347"
|
||||||
require «doc-gen4» from git
|
require «doc-gen4» from git
|
||||||
"https://github.com/jrpotter/bookshelf-docgen.git" @
|
"https://github.com/jrpotter/bookshelf-docgen.git" @
|
||||||
"ef54a19e670a19ee2a17a3bc70bfe4006b8e2a7a"
|
"b083d636c2581e72da9d18023240319dd5eca43a"
|
||||||
|
|
||||||
@[default_target]
|
@[default_target]
|
||||||
lean_lib «Bookshelf» {
|
lean_lib «Bookshelf» {
|
||||||
|
|
Loading…
Reference in New Issue