Skip to content

Commit

Permalink
Merge pull request #265 from leanprover/bump_bibtexquery
Browse files Browse the repository at this point in the history
chore: move BibtexQuery back to master
  • Loading branch information
kim-em authored Feb 3, 2025
2 parents 1213642 + aecc3ef commit f4d7240
Showing 1 changed file with 1 addition and 4 deletions.
5 changes: 1 addition & 4 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,8 @@ lean_exe «doc-gen4» {
require MD4Lean from git
"https://github.com/acmepjz/md4lean" @ "main"

-- Once https://github.com/dupuisf/BibtexQuery/pull/20 is merged, we can use this again:
-- require BibtexQuery from git
-- "https://github.com/dupuisf/BibtexQuery" @ "master"
require BibtexQuery from git
"https://github.com/kim-em/BibtexQuery" @ "bump_to_v4.17.0-rc1"
"https://github.com/dupuisf/BibtexQuery" @ "master"

require «UnicodeBasic» from git
"https://github.com/fgdorais/lean4-unicode-basic" @ "main"
Expand Down

0 comments on commit f4d7240

Please sign in to comment.