From 763784e1167905349e137535037ffc477db84a8d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 26 Jul 2022 15:17:56 +0200 Subject: [PATCH] fix: whenever you force push a kitten dies --- lakefile.lean | 2 +- lean_packages/manifest.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 6a1cd23..657a3b0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -25,7 +25,7 @@ require lake from git "https://github.com/leanprover/lake" @ "master" require leanInk from git - "https://github.com/hargonix/LeanInk" @ "doc-gen" + "https://github.com/hargonix/LeanInk" @ "doc-gen-json" module_facet docs : FilePath := fun mod => do let some docGen4 ← findLeanExe? `«doc-gen4» diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json index a039515..e0cb385 100644 --- a/lean_packages/manifest.json +++ b/lean_packages/manifest.json @@ -4,7 +4,7 @@ "rev": "112b35fc348a4a18d2111ac2c6586163330b4941", "name": "Cli"}, {"url": "https://github.com/hargonix/LeanInk", - "rev": "cb529041f71a4ea8348628a8c723326e3e4bdecc", + "rev": "5d0aaba8b4fceeaf3a719e014dd42ca5d02f4810", "name": "leanInk"}, {"url": "https://github.com/xubaiw/Unicode.lean", "rev": "1fb004da96aa1d1e98535951e100439a60f5b7f0",