diff options
| author | hallgren <hallgren@chalmers.se> | 2013-01-09 13:28:45 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2013-01-09 13:28:45 +0000 |
| commit | 1497fd863ae7b1d4b2c1f7144a1d2753875bae75 (patch) | |
| tree | b0ef46ada23c974e8b59492b73295ebcb6d4e9ab /src/runtime/python/pgf | |
| parent | 580e443a5eb731b50a84a7bc9aa9c3007d3a50f2 (diff) | |
PGF service: new command: download
This makes it possible to download PGF files from servers where the PGF service
is installed.
I am also considering making commmand=download the default instead of
command=grammar.
Diffstat (limited to 'src/runtime/python/pgf')
0 files changed, 0 insertions, 0 deletions