diff options
| author | Jesse Rosenthal <jrosenthal@jhu.edu> | 2016-12-13 19:35:07 -0500 |
|---|---|---|
| committer | John MacFarlane <jgm@berkeley.edu> | 2017-01-25 17:07:42 +0100 |
| commit | 5814096d79770edabc2822ff66747e3559c61e76 (patch) | |
| tree | 6a1f0c92740dccdc5516c47f3353b0d7c23f2362 /windows/make-windows-installer.bat | |
| parent | adcd4c5b7b116d59360f2e0e05472b3df98d1de2 (diff) | |
| download | pandoc-5814096d79770edabc2822ff66747e3559c61e76.tar.gz | |
Introduce DeferredMediaBag.
This is a lazy MediaBag, that will only be evaluated (downloaded/read
in) upon demand.
Note that we use fetchItem in getDefferedMedia at the moment to read
in/download. This means that we don't need to distinguish between URIs
and FilePaths. But there is an inefficiency here: `fetchItem` will pull
an item out of the mediaBag if it's already there, and then we'll
reinsert it. We could separate out `fetchItem` into the function that
checks the MediaBag and the underlying downloader/read-inner.
Diffstat (limited to 'windows/make-windows-installer.bat')
0 files changed, 0 insertions, 0 deletions