Manual: Only include the release number (e.g. 16.03)
This prevents gratuitous rebuilds of the manual every time the Git revision changes. Should help a bit with #17261.
parent
2a05368f
Please register or sign in to comment
This prevents gratuitous rebuilds of the manual every time the Git revision changes. Should help a bit with #17261.