Spring/spring-boot
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Polish "Make dev tools' home directory configurable"

Browse Source 
See gh-17924
This commit is contained in:
Andy Wilkinson
2021-07-16 13:13:17 +01:00
parent b9dbfad473
commit 8e7a6ceb44
3 changed files with 83 additions and 41 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
spring-boot-project/spring-boot-docs/src/docs/asciidoc/using/devtools.adoc
View File

@@ -285,6 +285,9 @@ For example, to configure restart to always use a <<using#using.devtools.restart
trigger-file: ".reloadtrigger"
----
By default, `$HOME` is the user's home directory.
To customize this location, set the `SPRING_DEVTOOLS_HOME` environment variable or the `spring.devtools.home` system property.
NOTE: If devtools configuration files are not found in `$HOME/.config/spring-boot`, the root of the `$HOME` directory is searched for the presence of a `.spring-boot-devtools.properties` file.
This allows you to share the devtools global configuration with applications that are on an older version of Spring Boot that does not support the `$HOME/.config/spring-boot` location.