error after renaming .lean files

Stream: lean4

[Paige Thomas]

I changed the names of some of the files in my project and updated the import paths for the files that use them. I am now getting the following error when I try to build the project.

pthomas@HP-Laptop:~/Desktop/github/lean/handbook_of_practical_logic_lean$ lake build
✖ [?/?] Computing build jobs
error: no such file or directory (error code: 2)
  file: ././././HandbookOfPracticalLogicLean/Chapter2/NF/DNF/ToDNF.lean
Some required builds logged failures:
- Computing build jobs
error: build failed

Is there a way to fix this other then deleting the repo, recloning it, and rebuilding it from scratch? I tried running lake clean, but the error persists.

[Paige Thomas]

Apologies, it turned out that I missed a file that was still using an old filename in an import. I guess I was expecting it to report the name of the file that had the error in it.