Mousewheel scrolling event in Mozilla

Did you know that Mozilla doesn’t fire the scroll event when you scroll a page with the mousewheel? Pretty annoying, that. However, I have just discovered that it does fire the DOMMouseScroll event. So, if you’re annoyed that using the mouse wheel doesn’t give you a scroll event, trap the DOMMouseScroll event instead, with window.addEventListener('DOMMouseScroll', scroll_function, false). Quite why this inconsistency exists escapes me a bit, but now there’s a solution.