summaryrefslogtreecommitdiff
path: root/device/ds_routines.c
diff options
context:
space:
mode:
authorSamuel Thibault <samuel.thibault@ens-lyon.org>2020-07-10 00:32:58 +0200
committerSamuel Thibault <samuel.thibault@ens-lyon.org>2020-07-10 00:32:58 +0200
commitb21966a525aad003d7434c5bc497ad29f827fbbb (patch)
tree15a5ce7b887cd1d4ee0ca68817fb9c82cc1f6c4a /device/ds_routines.c
parent1fac39d75bc57970ae173839e52f2d7d263d6c59 (diff)
parent821abb8d8138446db5485124c36cab5916077346 (diff)
Merge branch 'master-user_level_drivers2' into master-user_level_drivers2-debianmaster-user_level_drivers-debian
Diffstat (limited to 'device/ds_routines.c')
-rw-r--r--device/ds_routines.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/device/ds_routines.c b/device/ds_routines.c
index 36a8437e..28be3467 100644
--- a/device/ds_routines.c
+++ b/device/ds_routines.c
@@ -345,7 +345,7 @@ ds_device_intr_register (device_t dev, int id,
return D_NO_MEMORY;
// TODO The original port should be replaced
- // when the same device driver calls it again,
+ // when the same device driver calls it again,
// in order to handle the case that the device driver crashes and restarts.
err = install_user_intr_handler (&irqtab, id, flags, e);
if (err == D_SUCCESS)