Closed LouisSzeto closed 1 year ago
Check if shortcut /docs/v2/... exists in lean.io site.
/docs/v2/...
closes #1440
Not reporting non-existing link in lean.io
bug-<issue#>-<description>
feature-<issue#>-<description>
Description
Check if shortcut
/docs/v2/...
exists in lean.io site.Related Issue
closes #1440
Motivation and Context
Not reporting non-existing link in lean.io
Types of changes
Checklist:
bug-<issue#>-<description>
orfeature-<issue#>-<description>