diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-17 12:15:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 17:00:09 +0200 |
| commit | 2d8cbd7d4e5397a0c47c4dba9cfccac16ab66228 (patch) | |
| tree | d1c4baa471b6de4d09dbd34be4698be6adb19d1a /vernac/assumptions.ml | |
| parent | 13fb8de9aff07e4346ca4bdc866507503e9be12e (diff) | |
Fix install-doc target
Since 8995d0857277019b54c24672439d3e19b2fcb5af [make doc] puts css
files in subdirectories of doc/refman/html. These subdirectories cause
a failure when doing [install doc/refman/html/* target].
Diffstat (limited to 'vernac/assumptions.ml')
0 files changed, 0 insertions, 0 deletions