// works for .gif also. SCALE_DEFAULT has to be used
// (https://stackoverflow.com/questions/9392227/resizing-animated-gif-while-keeping-its-animation-using-java)
static ImageIcon resizeImageIcon(ImageIcon icon, int newW) {
  var img = icon.getImage();
  int newH = iround(img.getHeight(null)*(double) newW/img.getWidth(null));
  ret imageIcon(resizeImage_raw(img, newW, newH, Image.SCALE_DEFAULT));
}