[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#65401: 30.0.50; custom-theme-directory :type could be enhanced
From: |
Eli Zaretskii |
Subject: |
bug#65401: 30.0.50; custom-theme-directory :type could be enhanced |
Date: |
Sun, 20 Aug 2023 14:12:51 +0300 |
> Date: Sun, 20 Aug 2023 07:48:09 -0300
> From: Mauro Aranda <maurooaranda@gmail.com>
>
> The user option custom-theme-directory is supposed to hold a directory
> name. But its :type is a string.
>
> I realize that it isn't really a bug, but in order to offer better
> completion, at least, I'd like to change the type to be directory. So
> I'm filing this bug report to see if people would object to such a
> change.
Does the directory have to exist?
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Mauro Aranda, 2023/08/20
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced,
Eli Zaretskii <=
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Mauro Aranda, 2023/08/20
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Eli Zaretskii, 2023/08/20
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Mauro Aranda, 2023/08/20
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Eli Zaretskii, 2023/08/20
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Mauro Aranda, 2023/08/20
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Philip Kaludercic, 2023/08/21
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Eli Zaretskii, 2023/08/21
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Stefan Monnier, 2023/08/21
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Mauro Aranda, 2023/08/21
- bug#65401: 30.0.50; custom-theme-directory :type could be enhanced, Eli Zaretskii, 2023/08/26