From 49729f90f7de34840b75d936500bb0e1f76d9f01 Mon Sep 17 00:00:00 2001
From: adomani <adomani@gmail.com>
Date: Wed, 3 Apr 2024 20:32:13 +0200
Subject: [PATCH] Repetition and reverse

---
 scripts/mkAll.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/scripts/mkAll.lean b/scripts/mkAll.lean
index e783a23f5ff1e..404689c3753a1 100644
--- a/scripts/mkAll.lean
+++ b/scripts/mkAll.lean
@@ -71,10 +71,14 @@ def mkAllCLI (args : Parsed) : IO UInt32 := do
               | some lib => return #[lib.as! String]
               | none => getLeanLibs
   let mut updates := 0
-  for d in libs do
+  for d in libs.reverse do  -- reverse to create `Mathlib.Tactic` before `Mathlib`
     let fileName := addExtension d "lean"
     let fileContent ← getAll git d
-    if (! (←  pathExists fileName)) || (← IO.FS.readFile fileName) != fileContent then
+    if !(← pathExists fileName) then
+      IO.println s!"Updating '{fileName}'"
+      updates := updates + 1
+      IO.FS.writeFile fileName fileContent
+    else if (← IO.FS.readFile fileName) != fileContent then
       IO.println s!"Updating '{fileName}'"
       updates := updates + 1
       IO.FS.writeFile fileName fileContent