Skip to content

Change links to adapt to the repository name change #96

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 3 commits into from
Apr 23, 2026
Merged

Change links to adapt to the repository name change #96

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0a7a901
change links
RemyDegenne Apr 23, 2026
d68f1f0
bump docgen
RemyDegenne Apr 23, 2026
f31eeb4
change links
RemyDegenne Apr 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/blueprint.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ jobs:
./build_all.sh

- name: Compile blueprint and documentation
uses: leanprover-community/docgen-action@deed0cdc44dd8e5de07a300773eb751d33e32fc8 # 2025-10-26
uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14
with:
homepage: home_page
blueprint: true
Expand Down
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Fork the repository and create a new branch for your contribution. Make your cha

## What to contribute

See the [Roadmap](https://remydegenne.github.io/lean-bandits/roadmap).
See the [Roadmap](https://leanmachinelearning.github.io/roadmap/).

#### Finding tasks

Expand Down
6 changes: 3 additions & 3 deletions blueprint/src/web.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@

\graphcolor{mathlib}{purple}{The statement of this result is in Mathlib}

\home{https://RemyDegenne.github.io/lean-bandits}
\github{https://github.com/RemyDegenne/lean-bandits}
\dochome{https://RemyDegenne.github.io/lean-bandits/docs}
\home{https://leanmachinelearning.github.io}
\github{https://github.com/LeanMachineLearning/LML}
\dochome{https://leanmachinelearning.github.io/LML/docs}

\title{Lean Machine Learning}
\author{Rémy Degenne, Paulo Rauber}
Expand Down
80 changes: 0 additions & 80 deletions scripts/customize_template.py
View file
Open in desktop

This file was deleted.

10 changes: 0 additions & 10 deletions scripts/update.sh
View file
Open in desktop

This file was deleted.

4 changes: 2 additions & 2 deletions tutorial/Manual.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ def extraHead : Array Verso.Output.Html := #[

def config : RenderConfig := {
extraHead := extraHead,
sourceLink := some "https://github.com/RemyDegenne/lean-bandits",
issueLink := some "https://github.com/RemyDegenne/lean-bandits/issues",
sourceLink := some "https://github.com/LeanMachineLearning/LML",
issueLink := some "https://github.com/LeanMachineLearning/LML/issues",
}

def main := manualMain (%doc Manual.Front) (config := config)
8 changes: 4 additions & 4 deletions tutorial/Manual/Pages/Installation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,11 +28,11 @@ There are two ways to get the library depending on your needs:
Move to a directory where you want to store the library, then run:

```
git clone https://github.com/remydegenne/lean-bandits.git
cd lean-bandits
git clone https://github.com/LeanMachineLearning/LML.git
cd LML
```
This will create a local copy of the repository on your machine and move to the project directory.
We then need to buid the project.
We then need to build the project.
```
lake exe cache get
lake build
Expand All @@ -48,7 +48,7 @@ To use the library in your own Lean project (see the Lean installation instructi
```
[[require]]
name = "LeanMachineLearning"
git = "https://github.com/leanprover/lean-bandits"
git = "https://github.com/LeanMachineLearning/LML"
```

# Testing the installation
Expand Down
Loading