From 24f91f5762c4b3d9396387b0a66c65490e9ed327 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Wed, 14 Aug 2024 13:46:44 +0000 Subject: [PATCH] Include `lean_toolchain` to `files_to_add` list --- leanblueprint/client.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/leanblueprint/client.py b/leanblueprint/client.py index 3448ecb..6c5c2ac 100644 --- a/leanblueprint/client.py +++ b/leanblueprint/client.py @@ -449,6 +449,15 @@ def new() -> None: if home_page_created: files_to_add.append(jekyll_out_dir) + # Check if the 'lean-toolchain' file exists + lean_toolchain_path = Path(repo.working_dir) / "lean-toolchain" + if lean_toolchain_path.exists(): + # Check for differences between the 'lean-toolchain' file and the last committed version + diff = repo.git.diff("HEAD", "--", str(lean_toolchain_path)) + # If there are changes (the diff is not empty), add the file to the list of files to be committed + if diff: + files_to_add.append(lean_toolchain_path) + if not confirm("\nCommit to git repository?"): console.print("You are all set! Don’t forget to commit whenever you feel ready.") sys.exit(0)