Complete definitions directory option renaming

The renaming in commit 302f773 was incomplete, it was missing the
renaming of some references to the option.