• Raymond Toy's avatar
    Document how the cached gen directory works · af10e5d4
    Raymond Toy authored
    It's important that the manuals install to the gen directory which is
    cached.  When we deploy, we want to copy the gen directory to the
    public directory to get the docs.  Without this the manuals aren't
    part of the site anymore.  And if the manual hasn't changed, the
    cached gen directory has the manuals from the last time it was
    generated.
    af10e5d4
Name
Last commit
Last update
cmucl-www Loading commit data...
docs Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
README.md Loading commit data...
build-texinfo.sh Loading commit data...