diff options
| author | Ian Lynagh <ian@well-typed.com> | 2013-05-19 20:47:49 +0100 |
|---|---|---|
| committer | Ian Lynagh <ian@well-typed.com> | 2013-05-19 20:47:49 +0100 |
| commit | d15913bfcf44791a6c7668482dbc85d0e9102bb5 (patch) | |
| tree | 8aeab54aefb6651883f95e66eba3dd55ca2c3062 /resources/html/Ocean.std-theme | |
| parent | 74c66f5e30f9bb28cf45809958201680b186aeb0 (diff) | |
Use "cp -L" when making $(INPLACE_LIB)/latex too
Diffstat (limited to 'resources/html/Ocean.std-theme')
0 files changed, 0 insertions, 0 deletions