Paolo Teti 50ea70d7d0 Rename panic_implementation -> panic_handler ... panic_implementation has been deprecated/renamed. New name is panic_handler		2018-09-01 21:17:07 +02:00
..
panic-handler	Rename panic_implementation -> panic_handler	2018-09-01 21:17:07 +02:00