This repository has been archived by the owner on Aug 10, 2023. It is now read-only.
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Disable editor autocompletion for didactic reasons
In our educational environment, autocompletion is generally not desirable: * Beginners might be confused by the suggestions. * If we want students to memoize the keywords, suggesting them is counterproductive. Of course, autocompletion also has its benefits. If necessary, we can revisit this decision at a later time. For example, we could have different settings for beginner and complex tasks.
- Loading branch information