diff options
| author | hallgren <hallgren@chalmers.se> | 2014-01-09 14:18:21 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2014-01-09 14:18:21 +0000 |
| commit | ed1e662dea036e72f48e5362af6183c8f1cbcb08 (patch) | |
| tree | 13852301b7495c9bc9d9dd69a9eca5233389c261 /src/compiler/GF/Command | |
| parent | d8d78b61873fe715b82dc96e883a1262526cc255 (diff) | |
Check file datestamps before unioning PGF files
When running a command like
gf -make -name=T L_1.pgf ... L_n.pgf
gf now checks if T.pgf exists and is up-to-date before reading and computing
the union of the L_i.pgf files.
The name (T) of the target PGF file has to be given explicitly for this to work,
since otherwise the name is not known until the union has been computed.
If the functions for reading PGF files and computing the union were lazier,
this would not be necessary...
Diffstat (limited to 'src/compiler/GF/Command')
0 files changed, 0 insertions, 0 deletions