From a09f342faf63e3e09867121349ab7d782060acf0 Mon Sep 17 00:00:00 2001 From: grhkm21 <83517584+grhkm21@users.noreply.github.com> Date: Sun, 15 Oct 2023 11:54:35 +0100 Subject: [PATCH] Fix major typo This typo has caused me insuferable pain. --- DOCUMENTATION.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DOCUMENTATION.md b/DOCUMENTATION.md index 0c05de5..f6ad787 100644 --- a/DOCUMENTATION.md +++ b/DOCUMENTATION.md @@ -284,7 +284,7 @@ lake build Clone the game repository into a directory next to the game: ```bash cd .. -git clone hhttps://github.com/leanprover-community/lean4game.git +git clone https://github.com/leanprover-community/lean4game.git # or: git clone git@github.com:leanprover-community/lean4game.git ``` The folders `NNG4` and `lean4game` must be in the same directory!