various minor improvements (#638)

pull/1077/head
Simón Fishman 1 year ago committed by GitHub
parent b8d9b8c8a8
commit f11682c22b

File diff suppressed because one or more lines are too long
Loading…
Cancel
Save