From: Antonio Jimenez Pastor Date: Wed, 10 Jul 2019 08:37:45 +0000 (+0200) Subject: Merge branch 'master' of gitserver:pub/ajpastor/diff_defined_functions X-Git-Url: http://git.risc.jku.at/gitweb/?a=commitdiff_plain;h=d1f6ae1bbb82ce664104eab266cb133743cd19b4;p=ajpastor%2Fdiff_defined_functions.git Merge branch 'master' of gitserver:pub/ajpastor/diff_defined_functions --- d1f6ae1bbb82ce664104eab266cb133743cd19b4