For the record: > I did not know that Tjark had conversed with Florian privately before. > This removes the main accusation on his > http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was > looking like he was seizing control of the draft started by Florian.
The email reads (in German):
>> ich würde vorschlagen, dass ich Admin/download_components so
>> modifiziere, dass das Script Admin/components parsed (ähnlich wie in
>> init_components), um die herunterzuladenden Komponenten zu bestimmen.
>> Spricht aus deiner Sicht etwas dagegen?
>
> das Skript muss auch in der Lage sein, Komponenten der Vergangenheit
> runterzuladen. D.h. es würde über einen schalter -c/--current gehen,
> der dann einfach die aktuelle Liste runterlädt (oder vielleicht vorher
> noch die bereits vorhandenen Komponenten in ISABELLE_COMPONENTS noch
> davon wegnimmt?). Ansonsten würden nach wie vor die explizit
> angegebenen Komponenten runtergeladen.
>
> Ansonsten bleiben die Punkte, die bereits auf der Mailingliste genannt
> wurden:
> * curl statt wget
> * verschieben nach Admin/lib/Tools/download_components, um ein Tool der
> Admin-Komponente draus zu machen, und das Skript entsprechend anzupassen.
In this case, I did not follow the rule I normally impose on myself to
redirect any generic Isabelle issue to one of the mailing lists, this
was my fault.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
