From 4981d95741d711d164311a78f31f9bb690d12809 Mon Sep 17 00:00:00 2001
From: Martin Karlgren <marty@roxen.com>
Date: Thu, 5 Apr 2018 15:00:32 +0200
Subject: [PATCH] Filesystem.Monitor: Add set_stable_time() function.
---
lib/modules/Filesystem.pmod/Monitor.pmod/basic.pike | 13 +++++++++++--
1 file changed, 11 insertions(+), 2 deletions(-)
diff --git a/lib/modules/Filesystem.pmod/Monitor.pmod/basic.pike b/lib/modules/Filesystem.pmod/Monitor.pmod/basic.pike
index dc62c78e17..144515d989 100644
--- a/lib/modules/Filesystem.pmod/Monitor.pmod/basic.pike
+++ b/lib/modules/Filesystem.pmod/Monitor.pmod/basic.pike
@@ -1755,7 +1755,7 @@ void set_nonblocking(int|void suggested_t)
reschedule_backend_check(suggested_t);
}
-//! Set the @[default_max_dir_check_interval].
+//! Set the @[max_dir_check_interval].
void set_max_dir_check_interval(int max_dir_check_interval)
{
if (max_dir_check_interval > 0) {
@@ -1765,7 +1765,7 @@ void set_max_dir_check_interval(int max_dir_check_interval)
}
}
-//! Set the @[default_file_interval_factor].
+//! Set the @[file_interval_factor].
void set_file_interval_factor(int file_interval_factor)
{
if (file_interval_factor > 0) {
@@ -1775,3 +1775,12 @@ void set_file_interval_factor(int file_interval_factor)
}
}
+//! Set the @[stable_time].
+void set_stable_time (int stable_time)
+{
+ if (stable_time > 0) {
+ this::stable_time = stable_time;
+ } else {
+ this::stable_time = default_stable_time;
+ }
+}
--
GitLab