diff -r b0d6346b78ba -r b57b5cd21e95 devtools/extensions.st