]> git.tuebingen.mpg.de Git - paraslash.git/commitdiff
Merge branch 'maint'
authorAndre Noll <maan@tuebingen.mpg.de>
Sun, 21 Aug 2022 15:16:32 +0000 (17:16 +0200)
committerAndre Noll <maan@tuebingen.mpg.de>
Sun, 21 Aug 2022 15:16:32 +0000 (17:16 +0200)
Two fixes for para_play.

1  2 
interactive.c

diff --cc interactive.c
Simple merge