Closed kohlhase closed 8 years ago
I'm afraid wget
cannot check if it needs to download https://github.com/KWARC/MMT/raw/gh-pages/deploy/mmt.jar again because the directory is not browsable.
In https://github.com/KWARC/localmh/issues/279 wget -c -N
is recommended, but these options don't avoid reloading (only resume partial downloads) and @tkw1536 omitted them for now
./lmh/lib/packs/setups/MMT.py: proc = subprocess.Popen([wget_executable, self.mmt_jar_source, "-O", mmt_jar_path], stderr=sys.stderr, stdout=sys.stdout)
We need to test if this really changes something.
I get
Verbindungsaufbau zu raw.githubusercontent.com (raw.githubusercontent.com)|185.31.17.133|:443... verbunden.
HTTP-Anforderung gesendet, warte auf Antwort... 200 OK
Download der Datei schon vollständig; kein Download notwendig.
this looks good. (I hope it will pick up changes made to gh-pages.)
I also get
WARNUNG: Zeitstempel funktionieren nicht in Kombination mit der Option
»-O«. Genauere Erläuterungen finden Sie im Handbuch.
so maybe the option -N
should be omitted.
in my last update, it did not load MMT, but took a long time to determine that it was up to date. This seems OK from my side.
These options must be removed again. -N is ignored and -c will fail (or corrupt the file) when mmt.jar is updated.
Usually wget
preserves/takes the date of the file from the server, but github does not return a Last-Modified
header. Therefore this issue won't fix.
I suspect that it does not check if it needs to load.