You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It would be nice if this is made faster, because it slows down
the opening of new terminals for people who are used
to use a lot of them (because of the OPAM lines in ~/.bashrc).
Regards,
F.
The text was updated successfully, but these errors were encountered:
Right, now we are approaching 600 packages, I guess it's time to profile OPAM a little bit more carefully. So please, do not hesitate to report slow-down; you can also export OPAMSTATS=1 to get some raw stat numbers.
Hello,
It would be nice if this is made faster, because it slows down
the opening of new terminals for people who are used
to use a lot of them (because of the OPAM lines in ~/.bashrc).
Regards,
F.
The text was updated successfully, but these errors were encountered: