You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
While docs/public is included into .gitignore, it is somehow becomes tracked by git after Travis pushes it into repo at the end of the build cycle. Need to deal with this somehow otherwise too many html files get included into commits which is not necessary.
The text was updated successfully, but these errors were encountered:
Also, it seems that old links work and point to the old documetnation -- which means that the old files are not deleted when new documentation is compiled (see e.g Travis builds 88 and 87...). This is not good -- a new documentation push should completely wipe out an old one.
While docs/public is included into .gitignore, it is somehow becomes tracked by git after Travis pushes it into repo at the end of the build cycle. Need to deal with this somehow otherwise too many html files get included into commits which is not necessary.
The text was updated successfully, but these errors were encountered: