pin: fix update source of version-pinned package#3726

Merged

rjbou merged 1 commit intoocaml:masterfrom rjbou:pin-sources

Jan 25, 2019

+8-2

Commits on Jan 22, 2019

pin: update source of pinned directory
rjbou
committed