diff options
| author | hallgren <hallgren@chalmers.se> | 2014-03-19 16:15:05 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2014-03-19 16:15:05 +0000 |
| commit | b061d59044b0cc689cf270617364ab36c8a0792f (patch) | |
| tree | b3cf29ad4a7ae608be8b0de043fd055d7b046e5d /src/example-based/ExampleService.hs | |
| parent | cbb538e170c9a7233e2ca438db8560d60fd91609 (diff) | |
gf -server: add a command to manually flush the PGF cache
This can be used if the cloud service seems slow, but it would probably
be better to automatically expire unused PGFs from the cache after some time.
Diffstat (limited to 'src/example-based/ExampleService.hs')
0 files changed, 0 insertions, 0 deletions