Zulip Chat Archive

Stream: general

Topic: cache olean no longer working

Chris Hughes (Jun 24 2019 at 11:57):

Anybody else having this problem?

HEAD is now at d7283d7f feat(string): `split_on` a `char` (#1145)
Trying to fetch cached olean
.git/hooks/post-checkout: line 14: /Users/chrishughes/.mathlib/bin/cache-olean: Permission denied

Simon Hudon (Jun 24 2019 at 12:04):

Are you sure all the scripts in .mathlib/bin have execution permission? Try chmod +x ~/.mathlib/bin/cache-olean

Chris Hughes (Jun 24 2019 at 12:12):

Fixed thanks.

Simon Hudon (Jun 24 2019 at 12:15):

:+1:

Simon Hudon (Jun 24 2019 at 12:15):

The setup should really take care of the for you though

Scott Morrison (Jun 24 2019 at 22:21):

I had the same problem recently, actually. I wonder what happened.

Last updated: Dec 20 2023 at 11:08 UTC