Zulip Chat Archive

Stream: general

Topic: copy _target dir


view this post on Zulip Patrick Massot (May 28 2018 at 12:55):

I really don't understand how the _target directory works

view this post on Zulip Patrick Massot (May 28 2018 at 12:55):

I want to help Kevin so I clone his repo

view this post on Zulip Patrick Massot (May 28 2018 at 12:55):

Of course it depends on mathlib

view this post on Zulip Patrick Massot (May 28 2018 at 12:55):

So I try to copy _target from my own projects to avoid compiling mathlib

view this post on Zulip Patrick Massot (May 28 2018 at 12:55):

and it doesn't seem to work

view this post on Zulip Patrick Massot (May 28 2018 at 12:56):

or maybe it does

view this post on Zulip Patrick Massot (May 28 2018 at 12:56):

it seemed like VScode was taking forever to compile

view this post on Zulip Patrick Massot (May 28 2018 at 12:56):

which seemed like it was compiling lots of files

view this post on Zulip Patrick Massot (May 28 2018 at 12:56):

but maybe it was only Kevin's code

view this post on Zulip Johan Commelin (May 28 2018 at 13:02):

I have symlinked the _target dir before. It seems to work fine.


Last updated: May 13 2021 at 21:12 UTC