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
For building documentation locally, I comment out the call to deploydocs() from docs/make.jl. Of course, having 2 nearly identical Makefiles in the repository isn't ideal. Instead, this StackOverflow page gives some context on maintaining local versions of files:
git update-index --assume-unchanged docs/make.jl
will ignore local changes, but docs/make.jl is rewritten after a pull. Alternatively,
git update-index --skip-worktree docs/make.jl
does the same but persists after a pull. Neither command has any effect on other users; anyone who wants the same behaviour needs to run one of these commands locally before editing docs/make.jl.
No description provided.
The text was updated successfully, but these errors were encountered: