From 64f9723d43fc99a66f52625b346ccddf87b7acc6 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Fri, 16 Jun 2023 07:33:55 +0000
Subject: [PATCH] chore: teach lake exe cache about ProofWidgets (#5128)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
---
 Cache/IO.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Cache/IO.lean b/Cache/IO.lean
index be9a963d8b16f..b52fd2deddeb7 100644
--- a/Cache/IO.lean
+++ b/Cache/IO.lean
@@ -66,11 +66,13 @@ def isMathlibRoot : IO Bool :=
 def mathlibDepPath : FilePath :=
   LAKEPACKAGESDIR / "mathlib"
 
+-- TODO this should be generated automatically from the information in `lakefile.lean`.
 def getPackageDirs : IO PackageDirs := return .ofList [
   ("Mathlib", if ← isMathlibRoot then "." else mathlibDepPath),
   ("MathlibExtras", if ← isMathlibRoot then "." else mathlibDepPath),
   ("Aesop", LAKEPACKAGESDIR / "aesop"),
   ("Std", LAKEPACKAGESDIR / "std"),
+  ("ProofWidgets", LAKEPACKAGESDIR / "proofwidgets"),
   ("Qq", LAKEPACKAGESDIR / "Qq")
 ]