Remove the @[default_target] attribute from the lean4-metaprogramming-book library. This prevents it from being automatically built on a lake build, which does not work because it just builds all the code in the book (incuding errors). This will help prevent Reservoir from giving the book a red cross.
Also uses the now-more-standard where syntax rather than braces for the configurations.
Remove the
@[default_target]attribute from thelean4-metaprogramming-booklibrary. This prevents it from being automatically built on alake build, which does not work because it just builds all the code in the book (incuding errors). This will help prevent Reservoir from giving the book a red cross.Also uses the now-more-standard
wheresyntax rather than braces for the configurations.