diff php/pool.php @ 2427:b33d6988152c

Instructions update to reflect #71, also other minor things.
author Brecht De Man <b.deman@qmul.ac.uk>
date Fri, 27 May 2016 16:37:17 +0200
parents 169f08dc9634
children d26623bd65e0
line wrap: on
line diff