[Agda] Re: The standard library has moved to github

[Jason Gross]

The HoTT library <https://github.com/HoTT/HoTT> uses
Travis<http://travis-ci.org> to
do continuous integration, and build documentation and push it to
gh-pages<http://hott.github.io/HoTT/coqdoc-html/index.html>.
 The travis setup we use is
here<https://github.com/HoTT/HoTT/blob/master/.travis.yml>,
and this commit
message<https://github.com/HoTT/HoTT/commit/082425c2b6633dc66ebe2365b860e2ad88c5610f>
describes
how we generated the token that Travis needs.  If you run into trouble or
need help, I can probably provide answers.

(You could probably then just have that link redirect to the gh-pages
generated version.)

-Jason


On Fri, Jan 17, 2014 at 11:48 AM, Stevan Andjelkovic <
stevan.andjelkovic at strath.ac.uk> wrote:

> Ulf Norell <ulf.norell at ...> writes:
> >
> > [...]
> >
> > This also means that the library has its own issue tracker, so please
> send
> > library issues
> > to github rather than to google code. I'll work on migrating the existing
> > issues.
>
> Perhaps it would also make sense to migrate the html listings of the
> library:
>
>   http://www.cse.chalmers.se/~nad/listings/lib/Everything.html  ?
>
> It would be good if it stayed in sync with the repository (ideally via some
> post-hook?). Somebody familiar with github (and github pages?) can perhaps
> suggest how to best set this up?
>
>
> Cheers,
> SA.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140117/94fc5479/attachment.html