Skip to content

Avoid running a pager when running 'git diff'#3912

Merged
aalekseyev merged 2 commits intoocaml:masterfrom AltGr:no-pagerNov 17, 2020
+1-1

Commits

Commits on Nov 3, 2020

Commits on Nov 17, 2020