Christian,
On Wed, 2012-08-08 at 14:17 +0900, Christian Sternagel wrote:
the script you introduced in
http://isabelle.in.tum.de/repos/isabelle/rev/c895e334162c
is rather useful. How about also providing a variable (as TMP for the
download directory) to set the actual isabelle tool
On Wed, 2012-08-08 at 11:22 +0200, Makarius wrote:
One could also use wget -O- ... | tar xvzf - and avoid the TMP file.
Unfortunately, this doesn't behave as one would like when wget fails.
Best regards,
Tjark
___
isabelle-dev mailing list
On Wed, 15 Aug 2012, Tjark Weber wrote:
On Wed, 2012-08-08 at 14:17 +0900, Christian Sternagel wrote:
the script you introduced in
http://isabelle.in.tum.de/repos/isabelle/rev/c895e334162c
is rather useful. How about also providing a variable (as TMP for the
download directory) to set the
On Wed, 2012-08-15 at 13:22 +0200, Makarius wrote:
I will have to take a look at the component business again soon, to
simplify it further and remove features and clones of other Isabelle
scripts.
Great. I've now turned download_components into an isabelle (Admin)
tool (cf. 01d1734f779d), as
I'm recently getting
clemens-ballarins-macbook-air:IsarRef ballarin$ hg push
Password:
remote: Not trusting file
/home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user
wenzelm, group isabelle
pushing to
Hi Clemens,
clemens-ballarins-macbook-air:IsarRef ballarin$ hg push
Password:
remote: Not trusting file
/home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user
wenzelm, group isabelle
pushing to
Quoting Clemens Ballarin balla...@in.tum.de:
[...]
pushing to
ssh://balla...@macbroy2.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
searching for changes
remote: Not trusting file
/mnt/nfsbroy/home/isabelle-repository/repos/isabelle/.hg/hgrc from
untrusted user
