]> gitweb.factorcode.org Git - factor.git/commitdiff
Merge commit 'f681570c96fa7e9cdd7eeefba3903cdc1b5701b9'
authorJose A. Ortega Ruiz <jao@gnu.org>
Sat, 13 Dec 2008 16:52:43 +0000 (17:52 +0100)
committerJose A. Ortega Ruiz <jao@gnu.org>
Sat, 13 Dec 2008 16:52:43 +0000 (17:52 +0100)

Trivial merge