flush_extension_file  975 src/filemanager/cmd.c     flush_extension_file ();
flush_extension_file   23 src/filemanager/ext.h void flush_extension_file (void);
flush_extension_file  481 src/main.c         flush_extension_file ();    /* does only free memory */