You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
we ask contributors to run bibtool. However, bibtool is not available on this provided Codespace.
I was able to install it successfully with sudo apt update and sudo apt install bibtool, but ideally it would be provided as part of our Docker image or installed with a postCreateCommand automatically.
The text was updated successfully, but these errors were encountered:
I use GitHub Codespaces to contribute to mathlib, and realized today that at
mathlib4/docs/references.bib
Line 3 in 965c7f8
bibtool
. However,bibtool
is not available on this provided Codespace.I was able to install it successfully with
sudo apt update
andsudo apt install bibtool
, but ideally it would be provided as part of our Docker image or installed with apostCreateCommand
automatically.The text was updated successfully, but these errors were encountered: