forgot .ui in extra_dist
Authored by: Jean-Francois Dockes 2018-12-02
Parent(s): [b4ddb8]
Child(ren): [93cba5]