mDuo13
781f5bd6e9
Possible Jenkins build fix?
2020-01-06 16:17:58 -08:00
mDuo13
828e7c354f
PR-aware multi-language link checking(?)
2019-11-27 15:20:56 -08:00
mDuo13
10abd4b1cd
Language support updates
...
- Unicode header IDs filter
- Change some links to use the new ID formula
(It matches the GitHub-Flavored Markdown standard closely.)
- Build script changes
2019-11-05 23:08:41 -08:00
mDuo13
c466e85614
Fix all-target-link-checker var clash
2018-03-07 16:11:45 -08:00
mDuo13
d351f409c6
Fix bugs in PR-aware "Edit in GitHub" code
...
works around BashFAQ #050 etc.
2018-03-07 15:47:59 -08:00
mDuo13
5cd91c6f21
Branch/fork-aware Edit on GitHub links (2/2)
...
(Thrice-amended commit with proper bash syntax)
2018-03-07 15:16:29 -08:00
mDuo13
560c84f4f9
Fork/branch-aware edit on GH links, part 1/?
2018-03-07 14:41:33 -08:00
mDuo13
874b871422
Updates for new CI
2017-11-13 15:53:27 -08:00