"make" has to be run twice about unimath HOT 4 CLOSED

Could you please add this info to the README? V.

On Oct 29, 2014, at 2:34 PM, Daniel R. Grayson [email protected] wrote:

Starting from a fresh clone of the UniMath repository, typing "make" builds just "Coq", and
"make" must be run again to compile our files.

—
Reply to this email directly or view it on GitHub #40.

from unimath.

done.

On Wed, Oct 29, 2014 at 10:37 AM, Vladimir Voevodsky <
[email protected]> wrote:

Could you please add this info to the README? V.

On Oct 29, 2014, at 2:34 PM, Daniel R. Grayson [email protected]
wrote:

Starting from a fresh clone of the UniMath repository, typing "make"
builds just "Coq", and
"make" must be run again to compile our files.

—
Reply to this email directly or view it on GitHub <
https://github.com/UniMath/UniMath/issues/40>.

—
Reply to this email directly or view it on GitHub
#40 (comment).

from unimath.

The README says that it might be necessary for "make" to be run twice, but it does not say how one can know. Also, it seems to be needed consistently.
Hence I think it would be less confusing for people if they were simply instructed to run

make && make

like it is done in the Travis script.

from unimath.

That would be good, and it can't hurt. I was trying on an experimental
branch
to fix that misfeature and ran into a problem. I hope eventually to fix it.

On Mon, Mar 2, 2015 at 5:39 PM, Benedikt Ahrens [email protected]
wrote:

The README says that it might be necessary for "make" to be run twice, but
it does not say how one can know. Also, it seems to be needed consistently.
Hence I think it would be less confusing for people if they were simply
instructed to run

make && make

like it is done in the Travis script.

—
Reply to this email directly or view it on GitHub
#40 (comment).

from unimath.