aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/printers.mllib
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-05-27 11:50:11 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-05-28 13:50:43 +0200
commit5c437ab917bd24de66986e95dcf58c3f31e17a34 (patch)
tree500f703631f042df930e688b61247054269a5db3 /dev/printers.mllib
parentc6714db203f60413523ebeaac86242a6e4cc05e3 (diff)
STM: preserve branch name on edit (Close: #4245, #4246)
Diffstat (limited to 'dev/printers.mllib')
0 files changed, 0 insertions, 0 deletions